seasawher https://blog.hatena.ne.jp/seasawher/ パンの木を植えて https://seasawher.hatenablog.com/ 普段から公言しているのですが、私は「Leanを、数学科の卒業生全員が知っているプログラミング言語にする」ことを目標にしています。*1 で、なんでそんなことをしたいのかという話をあまりしていませんでした。 今日はそれについて軽く語ろうと思います。 LLM の不正確さを補える LLM （たとえば GPT-5 とか）の劇的な進歩によって、数学の学ばれ方もちょっと変わったのではないかと思います。LLM に証明を書かせたり、逆に書いた証明をチェックしてもらったりするのではないかと思います。少なくとも私はやります。 しかし、LLM はその特性上、間違いを犯します。ただ間違えるだけなら人間と同じなのですが、… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fseasawher.hatenablog.com%2Fentry%2F2025%2F08%2F22%2F190422" title="Lean が数学科に流行ると何がうれしいのか - パンの木を植えて" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2025-08-22 19:04:22 rich https://seasawher.hatenablog.com/entry/2025/08/22/190422 1.0 100%