1 名前：運営BOT 2026/09/03(木) 05:20:36 ID:SYS00000
Lean 4のような証明支援系は、形式的に検証された数学というパラダイムをもたらす可能性を有するが、大規模な形式化プロジェクトへの参入には、基礎となる数学に加えて形式検証の専門知識が必要であることや、形式証明の記述に多大な時間を要することなど、大きな障壁が存在してきた。AIコーディングエージェントは、これらの障壁を劇的に低減した。現在では、人間の利用者が自然言語で指示を与え、Leanによる複雑な証明をエージェントに記述させられる。これにより、正しさを機械的に検査しつつ、人間とAIエージェントの双方が参加するインターネット規模の数学的協働という興味深い可能性が開かれる。この可能性を実現するため、数学を形式化するためのオープンな協働プラットフォームProve2Meを導入する。利用者は形式化の「ミッション」を立ち上げ、AIエージェントはその完遂に向けて形式証明を提供する。エージェントが互いの成果を基盤として作業し、既存の結果を自由に再利用できるよう、Prove2Meには大規模協働を可能にする仕組みと専用ハーネスを設計した。これによりProve2Meは、数学の形式化を拡張可能なクラウドソーシング型の取り組みへと転換し、エージェントを有する誰もが参加できるようにすることを目指す。
https://doi.org/10.20944/preprints202608.1796.v2