Leonardo de Moura

Leonardo de Moura
Scientific career
Fields	Computer science
Institutions	AWS, Microsoft Research

Leonardo de Moura is a computer scientist, and creator of the Z3 Theorem Prover ^[1] and the Lean proof assistant during his time at Microsoft Research. ^[2] He currently works at AWS and is the Chief Architect at the Lean FRO. ^[3]

Awards and honors

• The 2007 CADE Skolem Award for the paper "Efficient E-Matching for SMT Solvers" that has passed the test of time, by being a most influential paper in the field. ^[4]
• The 2021 Computer Aided Verification Award for the field-changing contributions regarding his work on Z3. ^[5]
• The 2025 CADE Skolem Award for the paper "The Lean Theorem Prover (System Description)" that has passed the test of time, by being a most influential paper in the field. ^[4]
• The 2025 ACM SIGPLAN Programming Languages Software Award for his work on Lean. ^[6]

References

1. Hughes, Alyssa (2019-10-16). "Model-based approach behind Z3 theorem prover's efficiency, power". Microsoft Research. Retrieved 2025-06-15.
2. Roberts, Siobhan (2023-07-02). "A.I. Is Coming for Mathematics, Too". The New York Times. ISSN   0362-4331 . Retrieved 2025-06-15.
3. "Team — Lean FRO". lean-fro.org. Retrieved 2025-06-16.
4. "Skolem Award". cadeinc.org. Retrieved 2025-07-06.
5. "CAV Award | International Conference on Computer-Aided Verification". Archived from the original on 2025-06-01. Retrieved 2025-06-01.
6. "Programming Languages Software Award". www.sigplan.org. Archived from the original on 6 Jul 2025. Retrieved 2025-07-06.