数学の難問ABC予想、機械による検証プロジェクト始動　ZEN大など国際チームがLeanソフト活用

数学界の難問「ABC予想」、機械による検証プロジェクトが本格始動

私立のオンライン大学「ZEN大」（本部・神奈川県逗子市）は3月31日、数学の難問「ABC予想」を証明したとする京都大学数理解析研究所の望月新一教授の理論の正しさを、数学の証明支援ソフト「Lean（リーン）」を用いて検証する国際共同プロジェクトを開始したと正式に発表しました。

この画期的なプロジェクトには、オランダとカナダの大学も参加し、国際的な協力体制で進められます。プロジェクトチームは、2026年7月に中間報告を行うことを明らかにしており、数学界全体が注目する成果が期待されています。

望月新一教授の論文は2021年に京都大学数理解析研究所が編集する国際専門誌に掲載されましたが、その理論の正しさについては、現在でも世界中の数学者の間で意見が分かれたままとなっています。このプロジェクトは、長年にわたる学術的な論争に客観的な結論をもたらすことを目的としています。

—

ABC予想は、整数の足し算とかけ算の関係性に関する予想で、1985年に欧州の二人の数学者によって提唱されました。この予想は、数論における最も重要な未解決問題の一つとされ、その証明は数学の基礎に大きな影響を与える可能性を秘めています。

証明支援ソフト「Lean」の役割は、人間による証明の検証を補助し、論理的な誤りや抜け漏れを機械的にチェックすることにあります。これにより、複雑な数学的理論の客観的な検証が可能となり、学術界の信頼性向上に貢献することが期待されています。

ZEN大の関係者は、「このプロジェクトが成功すれば、数学研究の方法論に新たな基準をもたらすでしょう」と述べており、科学技術と伝統的な学問の融合が進む現代の研究環境を反映しています。