Historiquement, la validité d'un théorème reposait sur le consensus d'une élite capable de le relire. Cependant, certaines démonstrations contemporaines dépassent désormais les milliers de pages, rendant leur vérification impossible pour un cerveau humain seul. Des langages comme Lean transforment les raisonnements mathématiques en code informatique, permettant à une machine de garantir avec certitude absolue la justesse d'un théorème.

L'intégration de l'IA dans ce processus accélère drastiquement la recherche : des modèles de langage proposent des conjectures que des outils vérificateurs valident ou invalident automatiquement. Des projets d'envergure mondiale, menés notamment par Kevin Buzzard et Terence Tao, visent à numériser l'intégralité du corpus mathématique pour créer une base de savoirs lisible par les machines.

Cette mutation engendre des enjeux géopolitiques majeurs. La maîtrise de ces outils offre un avantage décisif en cryptographie, défense ou physique nucléaire. Elle soulève aussi des questions éthiques fondamentales : la beauté d'une démonstration subsiste-t-elle si elle n'est plus compréhensible par l'humain ? Les mathématiques, longtemps la dernière science purement humaine, risquent-elles de devenir une simple branche de l'informatique théorique ?