Axiom、有限単純群の分類をLeanで24日で形式化
数学AI企業のAxiomは、AxiomProverのエージェント群が有限単純群の分類定理をLeanで24日間で形式化し、完全な機械検証付き証明を初めて実現したと発表した。形式化の過程で34件の数学的な不整合も見つかった。
形式検証のニュースと分析
形式検証に関する製品動向と業界分析を全6件掲載しています。
Claude、OSS 123本にアセンブリ水準の証明を作成
AnthropicのFrontier Red Teamが、Claudeで123のオープンソースライブラリ・239のエントリポイントに対し、64MB未満の入力でクラッシュしないことをコンパイル済みRISC-V上で形式証明した。
フェルマー最終定理、Lean4で完全機械検証証明
Anthropicがフェルマー最終定理のLean 4完全機械検証済み証明をApache 2.0でオープンソース化。Mathlib上に構築し6万超モジュールを3系統の検証器で確認した。
バークレーのVero基準、完答は43件中27件
バークレーRDI研究所の新ベンチマーク「Vero」は、AIエージェントにLean 4リポジトリ全体の実装と証明を同時に求める。最高性能のモデルでも完全解決は43件中27件にとどまった。
OpenBMBが8B形式化モデルを全公開、32B勢に勝る
OpenBMBが数学の自動形式化パイプラインMathFormを一括公開。8BモデルとLean 4検証済みデータ約36.7万件、評価コードを無償公開し、複数の32B専用モデルを上回る成績を記録した。
OpenAI、Astraで10本の証明を公開
OpenAIはAstraの初公開シグナルとして、数学と理論計算機科学の10件の成果、249ページの論文、Lean証明書、推論記録を公開した。