Une introduction à la formalisation mathématique

Qu’est-ce que la formalisation ?

Formalisation

• À bas niveau, formaliser les mathématiques signifie écrire les axiomes des mathématiques dans un langage formel strict, puis utiliser un ordinateur pour vérifier les preuves ligne par ligne

• Ce n’est pas nouveau : cela a commencé avant même l’existence des ordinateurs

• Pour la plupart des mathématiciens, cela ne semble pas très intéressant

Les Principia Mathematica de Russell et Whitehead.

Assistants de preuve

• Aujourd’hui, la formalisation se fait avec des assistants de preuve

• Les assistants de preuve sont des langages de programmation qui permettent d’exprimer des concepts mathématiques

• Ils permettent d’écrire des mathématiques sous une forme lisible par un humain

Oubliez ça

Lean et mathlib

• Il existe plusieurs assistants de preuve (Rocq, Isabelle, Agda, ...) ; nous nous concentrerons sur Lean

• Lean a été créé par Leonardo de Moura chez Microsoft Research en 2013

• C’est un logiciel open source — la version actuelle est Lean 4

• Mathlib est la bibliothèque mathématique officielle de Lean

• Elle couvre les mathématiques au niveau d’un étudiant en fin de licence ou en première année de master

• Près de 2,5 millions de lignes de code, écrites par des centaines de personnes

Identité de Parseval : \dfrac{1}{2\pi}\int_{-\pi}^{\pi} |f(x)|^2 \, dx = \sum_{n=-\infty}^{\infty} |\hat f (n)|^2

Espaces condensés : \text{CompHaus}^{\text{op}} \Rightarrow \text{Set}

Pourquoi formaliser ?

• La formalisation oblige à penser de façon claire et précise.

• Elle révèle souvent le besoin de nouvelles abstractions.

• Elle oblige à mieux organiser les mathématiques et à éliminer le bruit inutile.

• Au bout du compte, ce processus mène à une compréhension plus profonde des mathématiques.

• Elle détecte des erreurs et des hypothèses cachées qui peuvent échapper même à des rapporteurs attentifs.

Filtres

Soient (u_n) et (v_n) deux suites réelles et \ell \in \mathbb{R}. Supposons que u_n \to \ell par valeurs supérieures et que v_n \to -\infty. Alors

u_n + v_n \to -\infty

Cela ressemble à un cas particulier d’un théorème sur la somme de deux suites. Mais de quel théorème, exactement ?

La bonne abstraction est la convergence suivant des filtres bien choisis. Ce langage a été introduit par Bourbaki pour traiter de manière uniforme différentes formes de convergence.

• Les filtres séparent l’algèbre de l’addition des nombreuses notions possibles de convergence.

• Un même théorème couvre alors la convergence usuelle, les limites à gauche ou à droite, et la divergence vers l’infini.

• En pratique, la formalisation rend ce choix d’abstraction incontournable.

Un assistant de preuve peut vraiment assister

Le Liquid Tensor Experiment a vérifié formellement un théorème récent issu des travaux de Peter Scholze et Dustin Clausen sur les mathématiques condensées.

« L’assistant de preuve Lean a vraiment été cela : un assistant pour naviguer dans l’épaisse jungle qu’est cette preuve. » — Peter Scholze

À la question de savoir ce qu’il avait appris d’autre de la formalisation : « Ce qui fait réellement marcher la preuve ! Quand j’ai écrit le billet de blog il y a six mois, je ne comprenais pas pourquoi l’argument fonctionnait, ni pourquoi il fallait passer des réels à un certain anneau de séries de Laurent arithmétiques. » — Peter Scholze

Comment formaliser ?

Trois façons de formaliser

• À la main : l’humain écrit énoncés et preuves en Lean

• Avec l’aide de l’IA : un human propose des étapes, l’IA dirige

• Autoformalisation : l’IA traduit seule un texte mathématique en Lean

Apprendre à formaliser

• Natural Number Game : un jeu interactif pour commencer, sur les entiers naturels

• Glimpse of Lean : un tutoriel plus rapide, avec des exercices en analyse, topologie et logique

• Mathematics in Lean : le livre de référence pour formaliser des mathématiques avec mathlib

• Theorem Proving in Lean 4 : les fondements logiques de Lean

Formaliser avec l’aide de l’IA

Formaliser avec l’aide de l’IA

• Claude Code ou Codex : un agent qui travaille directement dans le projet Lean : il lit et modifie les fichiers, lance Lean et corrige ses erreurs.

• Lean LSP : l’agent voit ce que voit un humain dans l’éditeur (buts, erreurs, types) et cherche des lemmes dans mathlib.

• lean4-skills : des skills pour Lean, des méthodes de travail que l’agent suit (prouver, ébaucher, réparer, simplifier…).

• Il est utile de demander à l’agent d’enregistrer dans des skills (fichiers SKILL.md) les méthodes de travail adaptées à nos besoins.

Autoformalisation

Autoformalisation

• L’autoformalisation consiste à laisser l’IA faire tout le travail de formalisation.

• Elle consomme beaucoup plus de tokens.

• Il est aujourd’hui possible d’autoformaliser des livres entiers ou des articles de recherche, s’ils ne sont pas trop éloignés de mathlib.

• Les énoncés doivent toujours être vérifiés par un humain.

Comment Lean vérifie-t-il une preuve ?

• La correction est vérifiée par le noyau de Lean, un petit composant de confiance.

• Des vérificateurs externes indépendants peuvent aussi vérifier les preuves Lean.

• Le système axiomatique standard de Lean est équivalent, en force de cohérence, à ZFC plus des univers.

• Pour chaque théorème, on peut examiner les axiomes dont il dépend et demander à un vérificateur externe de vérifier sa preuve.

• Il reste à vérifier que l’énoncé formel exprime bien les mathématiques que l’on veut.

Jusqu’où se fier à une preuve Lean écrite par un LLM ?

• Avec du code écrit par un LLM, le problème de la confiance est plus difficile : il faut traiter le LLM comme un adversaire.

• Le code peut être énorme et difficile à digérer : la formalisation par Claude du dernier théorème de Fermat compte 13 millions de lignes de Lean.

• Des outils comme Comparator vérifient que le LLM n’a pas « triché ».

• Des vérificateurs de preuves indépendants et des versions à jour de Lean protègent davantage contre les attaques, y compris celles qui exploitent des bugs du noyau jusque-là inconnus.

• Une relecture par des experts reste nécessaire : tous les résultats annoncés cet été ont fait l’objet d’une telle relecture.

Comparator : vérifier une preuve écrite par un LLM

Comparator compare une solution écrite par le LLM à un défi : l’énoncé, écrit par nous, avec sorry à la place de la preuve.

• Même énoncé : la solution prouve exactement l’énoncé du défi.

• Axiomes : la preuve n’utilise que les axiomes autorisés.

• Noyau : la preuve est revérifiée par le noyau de Lean, et éventuellement par des noyaux indépendants.

• Bac à sable : le code du LLM est compilé isolé, pour qu’un code malveillant ne puisse rien modifier.

• Limite : Comparator ne dit pas si l’énoncé est le bon ; le défi doit être relu par un humain.

Si l’énoncé s’écrit facilement avec mathlib seul, le défi tient en quelques lignes faciles à relire : on peut alors faire confiance à la preuve, quelle que soit sa longueur.

Autoformaliser en pratique

Je conseille de suivre la méthode de Scott Armstrong, avec ses fichiers de skills.

• On place les sources dans un dépôt GitHub privé, si possible plusieurs preuves du même résultat ; l’agent installe Lean, mathlib et les skills.

• Un agent « orchestrator » fait choisir la preuve la plus facile à formaliser, fait auditer ce choix, puis fait écrire un plan détaillé.

• La preuve devient un graphe de dépendances : les énoncés clés sont écrits en Lean, relus par plusieurs agents, validés par un humain, puis gelés.

Les instructions de Scott Armstrong

Son premier message à Claude Code, où XXX et YYY désignent le théorème visé :

You are the orchestrator for our lean formalization project – the goal is to formalize the XXX theorem on YYY. We have placed several papers in the /sources subfolder, these have different proofs of the theorem. We need to find the best proof which is most convenient for formalization. This will be your first task. Please launch a codex agent in yolo mode (in a tmux shell) set to GPT 6 Astra (high effort) to do the research on the best proof, and audit its findings with an Opus (high) subagent. Then have a Sonnet subagent write a detailed MD file (“blueprint.md”) with the proof outline. Let me know if you have questions before you begin. — Scott Armstrong (source)

La méthode de Scott Armstrong (suite)

• Des sous-agents écrivent les preuves en parallèle : des modèles bon marché (environ 80 % de code correct) et des modèles plus forts pour les audits et les lemmes difficiles.

• Seuls les énoncés gelés peuvent contenir sorry ; un énoncé modifié doit être réapprouvé.

• Une preuve n’est acceptée que si elle compile, si son énoncé n’a pas changé et si un autre agent l’a revérifiée par rapport à la source.

• À la fin, on supprime le code mort (environ 20 %) et on optimise le temps de compilation.

• Exemple : son article de 145 pages avec Vicol, formalisé en environ 36 heures (270 000 lignes de Lean).

• Côté matériel : un abonnement haut de gamme à Claude ou à ChatGPT, idéalement les deux ; les agents tournent dans tmux sur un serveur, dont il faut surveiller le processeur et la mémoire.

Projets collaboratifs : Tau Ceti

Avec l’IA, on peut aussi lancer de grands projets collaboratifs, où humains et agents travaillent ensemble.

• Tau Ceti est une bibliothèque Lean construite au-dessus de mathlib, soutenue par la Lean FRO et la Mathlib Initiative.

• Les humains écrivent les feuilles de route et les critères de relecture ; les agents écrivent le code et le relisent.

• But : des bases générales et réutilisables, pour que d’autres projets puissent atteindre la recherche (revêtements universels, groupes réductifs, EDP, homologie de Floer…).

• Chacun peut lancer un agent : il choisit une tâche, ouvre une contribution, qui est relue par d’autres agents puis vérifiée par les outils de mathlib.

Projets collaboratifs : Prove2Me

• Prove2Me : une plateforme où humains et agents transforment des résultats d’articles et de livres en preuves Lean vérifiées.

• Chaque mission découpe un résultat en petits énoncés Lean qui mènent au théorème principal ; un « capitaine » la propose et un humain en valide l’énoncé.

• N’importe qui peut connecter son agent pour résoudre des missions ; les preuves doivent compiler avec une version fixée de mathlib, sans sorry.

• Des milliers de missions, surtout en théorie des nombres, et des campagnes pour améliorer des bornes (mesure d’irrationalité de π, exposant de la multiplication matricielle…).

• Les résultats vérifiés rejoignent une bibliothèque publique, Formalpedia.