La vérification qu'une démonstration mathématique est juste

Thomas Hales avait soumis une démonstration en 1998. Au terme de quatre ans de travail, les rapporteurs ont indiqué qu'ils étaient certains à 99 pour cent de sa justesse et qu'ils ne pouvaient aller plus loin, ce qui décrit honnêtement la limite de la vérification humaine sur un long argument calculatoire. Hales a ensuite passé dix ans à rendre la preuve lisible par une machine. Depuis, l'assistant Lean a absorbé de larges pans des mathématiques modernes, et Kevin Buzzard a engagé en 2024 un effort de cinq ans pour formaliser le dernier théorème de Fermat. Ce qui est en litige, c'est l'étape de certification, où un assistant de preuve est désormais plus fiable qu'un rapporteur fatigué, tandis que décider qu'un énoncé mérite démonstration, qu'un raisonnement éclaire quelque chose et qu'un article doit paraître reste un jugement que personne n'a proposé de céder.