Leonardo de Moura
Leonardo de Moura | |
|---|---|
 | |
| Scientific career | |
| Fields | Computer science |
| Workplaces | AWS, Microsoft Research |
Leonardo de Moura is a Brazilian 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".[4]
- The 2021 Computer Aided Verification Award for his contributions regarding his work on Z3.[5]
- The 2025 CADE Skolem Award for the paper "The Lean Theorem Prover (System Description)".[4]
- The 2025 ACM SIGPLAN Programming Languages Software Award for his work on Lean.[6]
References
- ↑ Hughes, Alyssa (2019-10-16). "Model-based approach behind Z3 theorem prover's efficiency, power". Microsoft Research. Retrieved 2025-06-15.
- ↑ Roberts, Siobhan (2023-07-02). "A.I. Is Coming for Mathematics, Too". The New York Times. ISSN 0362-4331. Retrieved 2025-06-15.
- ↑ "Team — Lean FRO". lean-fro.org. Retrieved 2025-06-16.
- 1 2 "Skolem Award". cadeinc.org. Retrieved 2025-07-06.
- ↑ "CAV Award | International Conference on Computer-Aided Verification". Archived from the original on 2025-06-01. Retrieved 2025-06-01.
- ↑ "Programming Languages Software Award". www.sigplan.org. Archived from the original on 6 Jul 2025. Retrieved 2025-07-06.