En 1611, Kepler formule en trois lignes une conjecture sur la façon d'empiler des sphères. Quatre siècles plus tard, une machine vient de boucler la version la plus aboutie de cette question en cinq jours. Ce n'est pas une anecdote technique. C'est le signe que la mathématique vient de changer de régime.

Depuis Euclide, un théorème est vrai parce qu'une poignée de gens malins l'ont lu et trouvé bon. Cette convention silencieuse a tenu tant que les preuves faisaient quarante pages. Quand Wiles résout Fermat en sept cents pages, quand Hales soumet une démonstration que les Annals of Mathematics publient en avouant n'en être convaincus qu'à 99 %, la méthode classique avoue qu'elle ne suit plus. Le bug est dans le système, pas dans les individus.

C'est dans ce vide que s'engouffrent aujourd'hui des capitaux considérables. Harmonic AI, fondée par le patron de Robinhood, lève près de 300 millions de dollars sur un outil qui traduit des mathématiques en code formellement vérifiable. DeepMind, Math Incorporated, Alphabet — tous parient sur la même idée : la formalisation est le banc d'entraînement idéal pour apprendre à raisonner vraiment, pas seulement à prédire du texte.

Mais la même technologie qui vérifie une preuve de théorème peut certifier un firmware de drone ou un protocole cryptographique post-quantique. La mathématique n'est plus seulement un sujet académique. Elle est devenue un nouveau standard de qualité pour toutes les couches critiques du numérique.

Cet épisode suit le fil : de Kepler à Viazovska, de Voevodsky à Lean, du laboratoire à la doctrine militaire. Et pose une dernière question — quand la preuve n'est plus un texte qu'on lit mais un programme qu'on exécute, où va l'intuition qui permet de trouver la suivante ?

#philosophie