Leonardo de Moura
Computer scientist
From Wikipedia, the free encyclopedia
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]
FieldsComputer science
InstitutionsAWS, Microsoft Research
Leonardo de Moura | |
|---|---|
| |
| Scientific career | |
| Fields | Computer science |
| Institutions | AWS, Microsoft Research |
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]