数学におけるABC予想の望月新一の証明をめぐる10年にわたる論争が、コンピュータ形式化によって解決される可能性がある。望月は、500ページに及ぶ自身の著作をLeanプログラミング言語に翻訳して自動検証することを提案した。このアプローチは、数学コミュニティ内の対立する陣営間の溝を埋めることができるかもしれない。
論争は2012年に遡り、日本・京都大学の教授である望月新一がABC予想のための広範な500ページの証明を発表した。この40年もの問題は、整数全体に対する方程式a + b = cとその素因数間の関係に関するもので、フェルマーの最終定理のような定理に影響を及ぼす。望月の証明は、彼の複雑な超宇宙テイヒミュラー（IUT）理論に依存しており、多くの専門家が理解しにくいものだと感じた。
初期の熱狂は、検証努力が停滞するにつれて薄れた。2018年、ボン大学のピーター・シュールツとフランクフルトのゲーテ大学のヤコブ・スティックスが潜在的な欠陥を指摘したが、望月はこれを否定した。中央の権威がないため、数学界は分裂した：大多数の数学者が一方に、小さなグループが望月と京都の数理解析研究所に所属する他方に。
膠着状態を打破するため、望月は今、コンピュータ検証数学のための言語であるLeanでの証明の形式化を提唱している。7月の東京での会議に着想を得て、彼は最近の報告書で、Leanが数学の真理を「社会的・政治的ダイナミクス」から解放できると主張する。彼の言葉では、「[Lean]は…数学の真理を社会的・政治的ダイナミクスの軛から解放するという根本的な目標に関して意味のある進歩を達成するための最良の、恐らく唯一の技術である。」
専門家たちは可能性を見いだすが、慎重だ。ロンドン帝国大学のケビン・バザードは、「Leanで書かれていれば、狂気じゃないよね？論文の多くはとても奇妙な言語で書かれているが、Leanで書けるなら、少なくともその奇妙な言語は完全に定義されたものになるということだ。」と指摘する。ユトレヒト大学のヨハン・コミリンも、「IUTのなぜを理解したい、そして10年以上それを待っている。Leanはそれらの答えを理解するのに役立つだろう。」と付け加える。
しかし、タスクは膨大で、専門家チームを必要とし、数年かかる可能性がある。成功しても解釈に関する議論が終わるわけではなく、望月自身もLeanが社会的問題に「魔法の治療」を提供しないと認めている。バザードは楽観的だ：「ソフトウェアとは議論できない。」