LEAN · VÉRIFICATION FORMELLE
Lean est un assistant de preuve : il vérifie un raisonnement, pas à pas, contre des axiomes déclarés. À SGDL, nous tenons Lean pour un outil qui donne les moyens — une façon de donner de la vérifiabilité au raisonnement sur l’espace, en gardant l’auteur et la trace visibles. Non un oracle opaque qui rend une réponse que personne ne peut retracer.
Les machines produisent désormais plus de preuves que les mathématiciens n’en peuvent lire. La question n’est plus seulement de savoir si un résultat est vrai, mais pourquoi il l’est, et qui peut le retracer. Un résultat sans trace rompt la pratique scientifique : créditer le raisonnement, pas seulement la réponse.
Lean, pour nous, est un travail de grande valeur mais de bas niveau : s’assurer qu’un effort créatif — une conception, un modèle, une affirmation scientifique — est garanti, de façon prouvable, de tenir. Nous voulons faire partie d’une colonne vertébrale vérifiable, comme la statistique soutient une expérience : présente, sobre, vérifiable, au service de la compréhension du monde et de ses lois physiques.
Tout sur cette page est une seule chose : l’Arithmétique des Formes elle-même (Rotgé, Université de Montréal, 1997), formalisée en Lean 4 mur à mur. 1 962 théorèmes du noyau — la Partie I de l’inventaire, tirée de la thèse, des articles et des brevets — vérifiés par Lean 4 et Mathlib, re-vérifiables par une seule commande de compilation. Les applications bâties sur ce noyau sont comptées à part, et ne figurent pas ici.
À la racine, une seule idée. Tout point de l’espace est intérieur, frontière ou extérieur — un verdict ternaire, INT / FRO / EXT. Les solides ne sont pas des maillages ; ils s’écrivent, et se combinent en prenant le minimum ou le maximum de cette densité ternaire. Le verdict est exact — décidé sur les rationnels — et n’exige aucune coordonnée choisie à l’avance.
Collez deux solides le long d’une arête, ou en un seul point, et une représentation par maillage casse : à la jonction, un point n’a pas de voisinage en forme de disque — il est non-manifold, et un test dedans / dehors ordinaire devient indécidé. Le verdict de densité ne suppose aucune variété. Comme les solides se combinent par minimum et maximum, la jonction reste exactement classée — frontière est frontière, intérieur est intérieur — là où un maillage se déchirerait.
C’est une propriété de l’algèbre des densités elle-même, pas un cas particulier : aucune variété n’est supposée nulle part, et le verdict à la jonction est prouvé, ligne à ligne, dans le noyau.
Le noyau porte une lignée. Desargues et Pascal ont donné à la géométrie projective ses théorèmes ; l’Arithmétique des Formes de Rotgé (1997) a rendu algébrique l’écriture des solides exacts. Lean vérifie désormais toute la chaîne, ligne à ligne.
Nous intégrons un portefeuille de brevets de méthodes formelles de raisonnement sur l’espace dans des bibliothèques Lean, pour qu’elles soient réutilisées par de plus en plus d’outils de vérifiabilité et d’outils agentiques — chaque résultat portant sa propre trace re-vérifiable.
Ces méthodes ont été bâties pour outiller des humains sous fortes contraintes — comprendre et manipuler le monde dans des environnements complexes, d’une station spatiale à un rover planétaire. Rendue formelle sous Lean, cette expertise peut rayonner vers d’autres domaines : l’imagerie médicale, l’usage scientifiquement fondé des ressources naturelles, la planification. Une géométrie exacte, vérifiable, réutilisée.
