The Lean Language
Proving That a Program Is Correct
How can we be certain that a computer program contains no critical errors? In the traditional software industry, the answer relies primarily on testing. But testing a program never guarantees that no bugs remain.
Lean offers a different approach. More than just a programming language, it is also a proof assistant capable of mathematically verifying that a computer program functions correctly. Long confined to theoretical research, this promise is now at the heart of major scientific, industrial, and societal challenges.
Code is constantly evolving. Proofs must therefore be able to adapt to software rewrites.
Leonardo de Moura, computer science researcher and creator of Lean, chief architect and co-founder of the Lean Focused Research Organization (Lean FRO)
In practical terms, the system functions like a massive mathematical building block set. The researcher writes hypotheses, applies reasoning rules called “tactics,” and then Lean automatically verifies each step. If an error occurs, it is immediately detected. This approach is called “formal proof” and is transforming the way critical software is designed. Until recently, these methods were extremely time-consuming and required a great deal of expertise, involving significant programming effort. But the advent of AI is a game-changer, as it reduces the effort required.
Leonardo de Moura, computer science researcher and creator of Lean, chief architect and co-founder of the Lean Focused Research Organization (Lean FRO).
An international community
To secure the digital world
Created by computer science researcher Leonardo de Moura, Lean and the impressive possibilities it offers have given rise to a scientific and industrial community. Led by Emilio Jesús Gallego Arias, a senior research engineer at the Lean Focused Research Organization (Lean FRO)—of which Leonardo de Moura is chief architect and co-founder—the Lean Paris Meetup brought together researchers, engineers, developers, and industry professionals at Mines Paris – PSL around a single goal: to enable humans and machines to build rigorous mathematical proofs and verified software.
We want to create a space where ideas from research, industry, and collaborative development can come together and evolve side by side.
Emilio Jesús Gallego Arias, senior research engineer at the Lean Focused Research Organization (Lean FRO) and organizer of the Lean Paris Meetup
For Mines Paris – PSL, this event marks an important milestone in the development of a scientific ecosystem dedicated to formal methods and proof languages. By combining research, education, and industrial partnerships, the School is fully committed to this emerging, demanding, and promising movement.
Emilio Jesús Gallego Arias, senior research engineer at the Lean Focused Research Organization (Lean FRO) and organizer of the Lean Paris Meetup.
A meeting place
Between research, industry, and the open-source community
This approach is currently experiencing spectacular growth. Companies such as Amazon Web Services (AWS), Microsoft, Google, and Mistral AI are already using Lean to verify cryptographic libraries (i.e., sets of programs that perform encryption operations to protect data and ensure its confidentiality), compilers (software that translates code written by developers into machine language that computers can understand), and critical IT systems (where an error could have serious consequences).
One of the flagship projects is Signal Shot, an initiative launched jointly by the messaging app Signal, the Beneficial AI Foundation, and Lean FRO. Its goal is to mathematically verify Signal’s encryption protocol—that is, the mechanisms that protect users’ messages—as well as the software that implements it, written in the Rust programming language. Used to develop secure applications, Rust is renowned for its robustness and its ability to limit certain cybersecurity vulnerabilities. With more than 100 million people using Signal worldwide, formally demonstrating that these systems function correctly has become a major issue of digital trust.
Lean’s rise can also be attributed to the computational formalization of contemporary mathematics, which represents a major development. Today, Mathlib—Lean’s mathematical library—contains more than 270,000 formalized theorems and over two million lines of code. It involves more than 750 contributors worldwide. For research, the challenge is not only to verify proofs but also to transform the way people collaborate.
Proof via AI
Furthermore, a genuine convergence is emerging between AI and formal mathematics. At the Meetup, Roman Soletskyi, a researcher at Mistral AI, presented Leanstral, an open-source agent specifically designed for Lean 4. Its goal is to help write Lean code and build formal proofs more quickly. This development is taking place against the backdrop of a dramatic acceleration in the use of AI in mathematics and software verification. Consequently, the challenge is no longer just to produce code or proofs, but to be able to rigorously validate them.
Today, AI agents are already capable of writing proofs in Lean, suggesting optimizations, and even automatically restructuring entire libraries. One example is the ten AI agents that succeeded in building a specialized language—complete with comprehensive safety proofs—in just one weekend.
But this automation also reinforces, at the same time, the need for particularly robust validation mechanisms. This idea encapsulates one of the major contemporary challenges in formal proof: as software systems become increasingly autonomous and AI-generated, trust can no longer rely solely on traditional testing.
A Long-Standing Research Tradition at Mines Paris – PSL
While Lean may appear today as an emerging technology, the research that made it possible is part of a longer scientific history to which Mines Paris – PSL has contributed for several decades. At the CRI, work on typing systems for programming languages dates back to the 1990s. This research forms part of the theoretical foundations of modern proof assistants.
The CRI, particularly thanks to the contributions of Emilio Jesús Gallego Arias, then a postdoctoral researcher at the laboratory, has been working since 2013 on Rocq (formerly Coq) as part of the ANR Faust Environment Everyware project: a ubiquitous solution for portable, cross-platform digital audio processing—FEEVER, coordinated by CRI Emeritus Researcher Pierre Jouvelot and dedicated to digital audio processing. This software makes it possible to:
- express mathematical reasoning formally, that is, in a highly rigorous and unambiguous manner;
- automatically verify whether a mathematical proof is correct;
- assist researchers in constructing proofs by guiding them step by step;
- automatically generate “certified” computer programs—that is, programs guaranteed to be correct by mathematical methods.
Lean is heavily inspired by Rocq, but it now benefits from a new technological context, marked by the rise of AI and industrial needs for software verification.
Pierre Jouvelot, emeritus researcher at CRI
Olivier Hermant, a researcher at CRI, is thus participating in the development of Dedukti, a universal proof verifier co-developed with Inria Paris-Saclay. A key objective is to enable interoperability between different proof assistants such as Lean, Rocq, and Isabelle/HOL.
Training for the Proof Systems of Tomorrow
The ITN is helping to shape this ecosystem. By late 2025, the institute had already organized a “100% Lean” workshop for computer science instructors and several technical and industrial partners.
These workshops are designed to provide hands-on exposure to rapidly evolving technologies with promising potential.
Sébastien Boisgérault, faculty member and researcher at CAOR
Beyond research and industrial partnerships, the School intends to join this movement by integrating Lean into its curriculum. This development reflects a broader shift in how engineers are trained. In the future, it may no longer be enough simply to know how to program; one will also need to be able to mathematically prove that a software system is correct, robust, and secure. For ITN, this trend is fully in line with its mission to disseminate and experiment with emerging digital technologies.
There are currently particularly impactful synergies surrounding these technologies. The field remains relatively small, but its disruptive potential demands our attention, as this work has very concrete applications. The formal tools developed around Method B, for example—a formal method that enables reasoning about complex systems as well as software development—were used to design the software for Line 14 of the Paris Metro.
A New Culture of Proof
In a context where digital systems are becoming ubiquitous—whether in transportation, healthcare, cryptography, or AI—the ability to mathematically demonstrate that a program functions correctly is becoming a strategic imperative. As AI generates ever-increasing amounts of code and digital infrastructures govern critical systems, the challenge is no longer merely to create high-performance software, but to prove its reliability.
The hosting of the Lean Paris Meetup at Mines Paris – PSL thus illustrates a broader goal: to foster a meeting point between academic research, industrial innovation, and new applications. Mines Paris – PSL is thereby affirming its ambition to actively contribute to a new scientific culture of proof, where formal mathematics becomes a central tool for digital trust.
In a world where software controls critical infrastructure and where artificial intelligence generates ever-increasing amounts of code whose correctness remains open to question, the ability to formally verify the computer systems of tomorrow could become one of the major technological challenges of the coming decades.
Learn More
