Vérification de Preuve

Un différend de dix ans en mathématiques concernant la preuve de la conjecture ABC par Shinichi Mochizuki pourrait être résolu par une formalisation informatique. Mochizuki a suggéré de traduire son œuvre de 500 pages dans le langage de programmation Lean pour une vérification automatisée. Cette approche pourrait combler les divisions entre les camps rivaux de la communauté mathématique.