#lean のAIニュース

5件の記事

MathCode、数学問題から Lean 4 定理証明を自動生成するターミナル AI コーディングアシスタントとして公開

MathCode は、自然言語の数学問題を Lean 4 の定理に変換し、永続的な REPL や知識グラフを活用して自動証明を試みるターミナル型 AI コーディングアシスタントである。

Anthropic が未公開モデルを用いて、150 年以上未解決とされる数学の難問「リーマン予想」について従来の AI よりも大きな進歩を示した。

The Zvi は、OpenAI が未公開のモデル「Astra」が主要な数学問題 10 問を解決したと報告したが、その詳細や範囲については不明である。

Microsoft Research は、Rust、Aeneas、Lean、および AI エージェントを活用し、生成された暗号アルゴリズム（特にポスト量子暗号）が標準を正しく実装していることを形式検証で証明する手法を発表した。

2025 年、7 ヶ月目のスタートアップ企業「Axiom」が、難関の数学試験「プットナム試験」で全 12 問を解き、最優秀学生や既存 AI システムを上回る成績を収めた。