Great news!!!
Lean won the "SIGPLAN Programming Languages Software Award 2025". SIGPLAN is The ACM Special Interest Group on Programming Languages.
Congrats to Leonardo de Moura 🇧🇷, the Lean FRO team and the Lean community!!!
About the Award
The SIGPLAN Programming Languages Software Award is given by ACM SIGPLAN "to an institution or individual(s) to recognize the development of a software system that has had a significant impact on programming language research, implementations, and tools. The impact may be reflected in the widespread adoption of the system or its underlying concepts, by the wider programming language community either in research projects, in the open-source community, or commercially. The award includes a prize of $2,500."
The committee for this year was composed of: Niki Vazou, IMDEA (co-chair); Alexandra Silva (co-chair); Andrew Myers (observer); David Grove, IBM Research (SPLASH); Alastair Donaldson, Imperial (PLDI); Xavier Leroy, Inria (ICFP); and Amal Ahmed, Northeastern U (POPL).
The award was presented to
- Gabriel Ebner
- Soonho Kong
- Leo de Moura
- Sebastian Ullrich
The award slide reads:
"Citation: The Lean theorem prover is a remarkable software artifact. Grounded on strong theoretical and engineering foundations, Lean has had and continues to have a broad impact on industrial practice and scientific research. In particular, the Lean project has already had a significant impact on mathematics, hardware and software verification, and AI. It has gained substantial traction in the mathematics community with a user-developed library, Mathlib, that has more than 1.8M lines of code. The verification of foundational results at the request of Fields Medalist Peter Scholze and the verification of the Polynomial Freiman–Ruzsa Conjecture led by Fields Medalist Terence Tao have earned the system widespread recognition. It is clear that formal methods based on Lean will play a central role in mathematics in the years to come. Lean is also used in important verification projects in industry, including the verification of the Cedar access control language at AWS, the verification of the SampCert sampler for differential privacy at AWS, and blockchain verification projects at companies like StarkWare and Nethermind. Finally, with the success of projects like DeepMind’s AlphaProof and the adoption of Lean by startup companies like Harmonic, Lean has become the de facto choice for AI-based systems of mathematical reasoning."
PLDI'25 Award Ceremony
You can watch the award being presented at 9:22:58 in the "PLDI'25 Award Ceremony (June 19th)" livestream:
Leonardo de Moura's talk at PLDI
Before the award ceremony, Lean's Chief Architect Leonardo de Moura gave a keynote talk at the 46th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2025) in Seoul. His talk, titled "Lean: Machine-Checked Mathematics and Verified Programming, Past and Future," begins at 55:31 of the livestream:
Previous Winners
Who has won this award before?
- Rust
- OCaml
- Scala
- Racket
- GCC
- Coq
- Glasgow Haskell Compiler
- LLVM Compiler Infrastructure
And Leo had already won it before with the Z3 theorem prover.
Leonardo de Moura interviews
In English
Type Theory for All, by Pedro Abreu
Building Better Systems
In Portuguese
I have interviewed Leonardo twice.
Fronteiras da Engenharia de Software
Professor Adolfo Neto
Lean introduction talk
As part of the Esquenta SE4FP series, there will be an online talk in Portuguese by Sofia Rodrigues on the Lean programming language and theorem prover. Sofia is a Research Software Engineer at Lean FRO. The talk takes place on Wednesday, June 25, 2025, at 4:00 PM (UTC-3). The registration form is available at: https://forms.gle/gXQyGLeMKmDHfhSb8.
A Bluesky post
"LEAN won the award for programming language software :)" at PLDI'25, told me Sofia Rodrigues!!!
@lean-lang.org #LeanLang #LeanProver #Lean4🥳🎉🇧🇷🎊🍺
— Adolfo Neto (@adolfont.github.io) June 19, 2025 at 2:08 PM
[image or embed]
Top comments (0)