A programming language
Lean compiles to fast native code. Lean itself is written in Lean, and so is the generator of this website.
What Lean is
Lean is a programming language and a proof assistant. Leonardo de Moura started it at Microsoft Research in 2013; today it is developed by the Lean FRO, a non-profit, together with a large open-source community. In Lean, a statement and its proof are code: if the proof has a gap, the program does not compile.
A proof assistant
Definitions, statements and proofs are checked by a small trusted kernel. A wrong step is rejected, whoever or whatever wrote it.
A shared library of knowledge
Mathlib, the community library, gathers a large part of modern mathematics in checked form, maintained in the open by hundreds of contributors.
Orchestrating knowledge in the age of AI
Language models write fluently, but fluency is not correctness. When AI agents draft contracts, policies, code or analyses for your organisation, someone has to check them. Lean moves part of that checking from people to a machine that does not get tired.
State the rules precisely
A retention policy, an access rule or a pricing formula becomes a definition with one meaning, instead of a paragraph open to interpretation.
Let AI propose, let Lean check
An AI agent can draft a program or a proof. Lean accepts it only if it is correct, so you can use the speed of AI without trusting it blindly.
Keep an auditable trace
Checked definitions and proofs are plain files. They can be versioned, reviewed and re-checked by anyone, on your own infrastructure, years later.
A rule checked every time this site is built
This website is written in Lean with Verso. The file below is part of it: it states a data-retention rule and proves that purging old documents always respects it. If the proof were wrong, the site would not build, and would not be published.
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
Why Lean, and why us
Paul-Olivier Dehaye, founder of Hestia.ai, is a mathematician. He earned his PhD in number theory at Stanford University in 2006, under Daniel Bump, then was a junior research fellow at Merton College, Oxford, Heinz Hopf Lecturer at ETH Zurich and SNSF Assistant Professor at the University of Zurich. He has long been involved in open-source software for mathematical research.
He then turned the same rigour to data: reverse engineering data ecosystems, and leading the investigation into the Facebook-Cambridge Analytica scandal. Both careers teach the same lesson: a claim counts when it can be checked.
At Hestia.ai, we bring that lesson to Swiss SMEs. We use Lean to state the rules your AI systems must follow, to check what AI agents produce against them, and to keep the evidence under your control.