Anthropicがフェルマーの最終定理の形式化に挑戦！AIによる定理証明

Anthropicが、フェルマーの最終定理を「形式化」するプロジェクトを進めている。数学の証明をプログラミング言語（Lean 4）で記述し、コンピュータが検証できる状態にするのだ。この定理は1995年にアンドリュー・ワイルズが証明したが、人間が書いた数百ページの証明には常に「見落としや曖昧さがあるかもしれない」という可能性が付きまとっていた。それを完全に厳密にしようとしている。AIが膨大な補完作業と証明の探索をし、人間の負担を減らす試みだ。

ここで注目すべきは、これが単なる数学のパズルではなく、実務レベルのソフトウェア検証技術だということだ。AIが「自然言語の数学証明」を「ルールに厳密なプログラムコード」に翻訳できるなら、それは「曖昧な仕様」を「バグのない実装」に変換する道筋も示唆している。スマートコントラクト、医療機器、自動運転システム――複雑さが増すほど「人間の目による検証」では漏れが生じる領域で、この技術が活躍する可能性がある。AIが「正確さを求める作業」に向いているなら、その強みを形式検証に活かす発想は自然な流れだ。

「AIが書いたコードは検証が必須」という意識が浸透しつつある。やがて、AIとの組み合わせで「検証不可能なシステム」を作る時代から「検証できなければそもそも動かさない」時代へシフトしていく。その時、あなたの会社はそのルールに対応できるか。検証フレームワークの整備が、明日の競争力になる。