数学者がLean定理証明器に知るべきこと：信頼性とAIの衝撃

Leanカーネルにまた健全性のバグが見つかる日は来るのだろうか？

ソフトウェア開発者からすれば、この問いは正気とは思えない。過去にもバグはあったし、当然これからももっと出てくるだろう。

そうしたバグを見たとき、AIによるLean証明にとってそれは何を意味するのか？我々はそれを信頼できるのか？

この話は結局のところ、信頼に行き着く。

我々は人間による検証を非常に信頼できるものとして扱える。それはコミュニティと評判、そして人間によるproof-of-workがあるからだ。人間は数学の結果について時に嘘をつくが、そうした理由からそれは稀だ。人間は間違いを犯すが、その間違いはコミュニティによって発見される。そしてそのコミュニティ自体も、同じ理由でおおむね信頼できる。

LLMは評判など気にしない。頻繁にハルシネーションを起こし、でっち上げる。ハーネスの中では文字通りズルをしてルールを曲げようとする。これはルールにエンコードされた知識にとっては災難だ。だから我々はproof checkerに頼らざるを得ない。

問題は、proof checkerはどれほど信頼できるのか？バグはあるのか？そしてその根底にある理論自体が、悪用可能なパラドックスや不可知なもの、数学的な「バグ」から自由なのか？他の数学者を騙すことに固執した人間の数学者がいたと想像してほしい——検証器があったとしても、我々はその人の画期的成果を信頼するだろうか？

こうした性質のため、最後の最後の砦は人間でなければならず、それはコミュニティとproof-of-workに基づく人間の信頼システムに根ざしていなければならない。現時点で人々はツールを信頼しすぎている。

予測：Navier-Stokesの証明に疑問を投げかけるバグが、AIツールを使った人間によって見つかるだろう。