ABC予想

数学におけるABC予想の望月新一の証明をめぐる10年にわたる論争が、コンピュータ形式化によって解決される可能性がある。望月は、500ページに及ぶ自身の著作をLeanプログラミング言語に翻訳して自動検証することを提案した。このアプローチは、数学コミュニティ内の対立する陣営間の溝を埋めることができるかもしれない。