Un langage de programmation
Lean se compile en code natif rapide. Lean est lui-même écrit en Lean, tout comme le générateur de ce site.
Qu’est-ce que Lean ?
Lean est à la fois un langage de programmation et un assistant de preuve. Leonardo de Moura l’a lancé chez Microsoft Research en 2013 ; il est aujourd’hui développé par la Lean FRO, une organisation à but non lucratif, avec une large communauté open source. En Lean, un énoncé et sa preuve sont du code : si la preuve a une faille, le programme ne compile pas.
Un assistant de preuve
Définitions, énoncés et preuves sont vérifiés par un petit noyau de confiance. Une étape fausse est rejetée, quel qu’en soit l’auteur, humain ou machine.
Une bibliothèque de savoir partagée
Mathlib, la bibliothèque de la communauté, rassemble une grande partie des mathématiques modernes sous forme vérifiée, maintenue ouvertement par des centaines de contributeurs.
Orchestrer le savoir à l’ère de l’IA
Les modèles de langage écrivent avec aisance, mais l’aisance n’est pas l’exactitude. Quand des agents d’IA rédigent contrats, politiques, code ou analyses pour votre organisation, il faut les vérifier. Lean confie une partie de cette vérification à une machine qui ne se fatigue pas.
Énoncer les règles précisément
Une politique de conservation, une règle d’accès ou une formule de prix devient une définition au sens unique, plutôt qu’un paragraphe ouvert à l’interprétation.
L’IA propose, Lean vérifie
Un agent d’IA peut rédiger un programme ou une preuve. Lean ne l’accepte que s’il est correct : vous profitez de la vitesse de l’IA sans lui faire aveuglément confiance.
Garder une trace auditable
Définitions et preuves vérifiées sont de simples fichiers. On peut les versionner, les relire et les revérifier, sur votre propre infrastructure, des années plus tard.
Une règle vérifiée à chaque construction de ce site
Ce site est écrit en Lean avec Verso. Le fichier ci-dessous en fait partie : il énonce une règle de conservation des données et prouve que la purge des anciens documents la respecte toujours. Si la preuve était fausse, le site ne se construirait pas, et ne serait pas publié.
Examples/Retention.lean-- A data-retention rule, written so that Lean can check it.
structure Document where
ageInDays : Nat
structure Policy where
limitInDays : Nat
-- A document may be kept only while it is younger than the limit.
def Policy.allows (p : Policy) (d : Document) : Prop :=
d.ageInDays ≤ p.limitInDays
def Policy.purge (p : Policy) (docs : List Document) : List Document :=
docs.filter fun d => d.ageInDays ≤ p.limitInDays
-- After a purge, every remaining document is allowed by the policy.
theorem purge_respects_policy (p : Policy) (docs : List Document) :
∀ d ∈ p.purge docs, p.allows d := by
intro d h
simp [Policy.purge, List.mem_filter] at h
exact h.2
def thirtyDays : Policy := { limitInDays := 30 }
-- A 12-day-old document is allowed under a 30-day policy.
example : thirtyDays.allows { ageInDays := 12 } := by
unfold Policy.allows thirtyDays
decide
Pourquoi Lean, et pourquoi nous
Paul-Olivier Dehaye, fondateur de Hestia.ai, est mathématicien. Il a obtenu son doctorat en théorie des nombres à l’Université Stanford en 2006, sous la direction de Daniel Bump, puis a été junior research fellow au Merton College d’Oxford, Heinz Hopf Lecturer à l’ETH Zurich et professeur assistant FNS à l’Université de Zurich. Il s’implique depuis longtemps dans les logiciels open source pour la recherche mathématique.
Il a ensuite appliqué la même rigueur aux données : rétro-ingénierie des écosystèmes de données, et direction de l’enquête sur le scandale Facebook-Cambridge Analytica. Les deux parcours enseignent la même leçon : une affirmation compte quand on peut la vérifier.
Chez Hestia.ai, nous apportons cette leçon aux PME suisses. Nous utilisons Lean pour énoncer les règles que vos systèmes d’IA doivent suivre, pour vérifier ce que produisent les agents d’IA, et pour garder les preuves sous votre contrôle.