University of Toronto Mathematician Daniel Litt Says AI Proof Generation Limited by Verification Capability

Le mathématicien Daniel Litt de l'University of Toronto pointe un goulot d'étranglement fondamental dans les capacités mathématiques de l'IA : ce n'est pas la génération de texte ou de preuves qui pose problème, mais la vérification fiable de leur exactitude. Lorsque les preuves demeurent courtes, les modèles admettent facilement leurs erreurs s'ils sont pressés de justifier ; mais dès que les textes deviennent suffisamment longs, avec définitions, lemmes, classifications et références croisées, les erreurs s'obscurcissent et l'absence d'un mécanisme de cohérence globale stable empêche toute détection.

Litt illustre ce problème par un article de 800 pages généré par IA prétendant résoudre la conjecture de résolution des singularités en caractéristique positive — un problème fondamental en géométrie algébrique. Bien qu'il n'ait pas encore localisé des erreurs spécifiques, il considère ce texte invalide comme preuve formelle : si la conclusion était vraie, ce serait une percée majeure, or ni les experts humains ne l'ont examiné en détail, ni aucun modèle ne dispose de la capacité à auditer l'ensemble du raisonnement complexe et à vérifier indépendamment les conclusions.

Cet avis marque une évolution de Litt, qui reconnaît que l'IA a progressé davantage qu'il ne l'anticipait. Il identifie néanmoins le « raisonnement vérifiable en longues chaînes » comme la frontière séparant la résolution locale de la recherche mathématique autonome. Sur le plan économique, cette analyse suggère que les investissements s'orienteront vers la vérification formelle, les assistants de preuve (Lean, Coq, Isabelle) et l'infrastructure de données, plutôt que vers de simples modèles générant des textes plus longs.