m-hiyama https://blog.hatena.ne.jp/m-hiyama/ 檜山正幸のキマイラ飼育記 (はてなBlog) https://m-hiyama.hatenablog.com/ 雑記／備忘 2023-03-25 のブログ記事「証明支援系がダメだった理由と、AIでブーストする理由」の最後の節を、ちょっと長いですが引用します。 以上に述べたような事情で、5年10年のレンジで見れば、証明ソフトウェアが普及することはないだろうと思っていました。一般の人（特別な資質と情熱の持ち主ではない！）が、教育目的や、ソフトウェア検証の目的で証明ソフトウェアを使うのは無理だ、と。 しかし、最近の幾つかの記事で指摘したように、にわかに事情が変わってきました。 近未来の証明ソフトウェアは‥‥ 近未来の証明ソフトウェアはこうなる（といいな） チャットAIで形式証明も自然言語混じりで書ける（はず） 自然言語証… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fm-hiyama.hatenablog.com%2Fentry%2F2025%2F11%2F28%2F201730" title="AI支援形式証明への道 - 檜山正幸のキマイラ飼育記 (はてなBlog)" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://www.chimaira.org/img7/comet-proof.png Hatena Blog https://hatena.blog 2025-11-28 20:17:30 rich https://m-hiyama.hatenablog.com/entry/2025/11/28/201730 1.0 100%