Axabra Lean
Formaliser un raisonnement mathématique consiste à transformer les objets, hypothèses et transitions en définitions vérifiables. Lean permet ensuite de relire la chaîne de preuve ligne par ligne.
L’objectif n’est pas de décorer une preuve : il faut identifier les objets, les hypothèses minimales et les dépendances mathlib.
import Mathlib namespace Axabra -- A theorem becomes useful when its assumptions are explicit. theorem structured_bound {E : Type*} [LinearOrderedRing E] (a b c : E) (ha : a ≤ b) (hb : b ≤ c) : a ≤ c := by exact le_trans ha hb end Axabra
Méthode
Lean impose une discipline utile : chaque intuition devient un objet typé, chaque transition devient un lemme, chaque preuve doit survivre à la vérification.
On commence par séparer la donnée brute, la structure mathématique et les propriétés attendues. Cette étape évite les preuves trop fragiles.
Chaque bloc doit expliquer pourquoi une implication est vraie, avec des hypothèses nommées et des imports justifiés.
La formalisation est aussi une carte : elle montre les nœuds essentiels, les raccourcis dangereux et les zones encore conjecturales.
Architecture Lean
L’enjeu est de transformer un raisonnement ambitieux en une chaîne de définitions, de lemmes et de certificats que Lean peut contrôler sans ambiguïté.
Choisir les structures Lean les plus proches du raisonnement : ordre, treillis, graphes, espaces normés, anneaux, corps ou objets combinatoires finis.
Extraire les résultats réutilisables avant d’attaquer le théorème final. Un bon lemme Lean doit être court, nommé proprement et stable.
Présenter côte à côte la preuve humaine, la structure formelle et les limites restantes, sans confondre calcul expérimental et démonstration.
Showcase
Un certificat Lean est un petit objet vérifiable : soit il prouve une implication, soit il donne un contre-modèle fini lorsque l’implication est fausse.
Les certificats d’ordre 5 présentés ici couvrent les deux côtés du raisonnement : 10 implications sont certifiées vraies par preuve formelle, et 10 implications sont certifiées fausses par construction de magmas finis.
Pour un lecteur non spécialiste, l’intérêt est simple : le résultat ne dépend pas d’un commentaire ou d’une intuition. Le juge Lean relit le fichier, vérifie les types, les hypothèses et la conclusion. Si une implication échoue, le contre-exemple est lui aussi contrôlé.
Le point remarquable est cette symétrie : prouver et réfuter passent par le même niveau d’exigence. C’est précisément ce qui rend Lean utile pour des problèmes combinatoires difficiles.