本当に素晴らしい応用分野がたくさんあると思います。目指すべきことの一つは、証明可能な安定性、安全性、そしてハッキング不可能なソフトウェアを持つことです。ソフトウェアに関する数学的な証明を書いて、「このコードは、これらのユニットテストに合格するだけでなく、このような方法でハッキングしたり、メモリをいじったりすることができないことを数学的に証明できます」と言えるようになります。ハッカーが使うようなハッキング方法や、このような特性を持つものなどです。同じLeanと証明手法を使って、形式検証済みのソフトウェアを作ることができます。

これは、AIが世界をハッキングするあらゆる分野に関連する、非常に強力なサイバーセキュリティの要素になると思います。リーマン予想を証明できれば、非常に複雑なソフトウェアに関する途方もなく複雑な事柄も証明できるようになります。そうすれば、LLMに「正しいと証明できるソフトウェアを合成してください」と頼めるようになるでしょう。