Leonardo de Moura

Leonardo de Moura
Scientific career
FieldsComputer science
InstitutionsAWS, 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. ^ a b "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.
This article is issued from Wikipedia. The text is available under Creative Commons Attribution-Share Alike 4.0 unless otherwise noted. Additional terms may apply for the media files.