Leonardo de Moura

Creator of Lean and Chief Architect and co-founder of the Lean FRO. Brazilian computer scientist; currently a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services, previously at Microsoft Research and SRI International.

He started Lean in 2013 at Microsoft Research. Before that he created Z3, the SMT solver that sits under a large fraction of everything else in automated reasoning — which makes him the author of both an industrial-strength automatic solver and the interactive assistant this wiki tracks, the two halves of the split Lean's own page draws between finding a proof and checking one.

The 2025 Skolem Award went to the 2015 CADE paper "The Lean Theorem Prover (System Description)", and Lean took the 2025 ACM SIGPLAN Programming Languages Software Award. Both are retrospective prizes for work whose adoption arrived a decade later, which is the shape cluster F keeps finding: tech-adoption-curve-twenty-years reports that most significant post-2000 technologies were never flagged early.

His current employer, AWS, both ships Lean-verified software (Cedar, SampCert) and made the largest donation in the FRO's history. Noted so a reader can weigh the AWS endorsements on the Lean site with that in view.

Related

lean-theorem-prover · lean-fro · mathlib · lean-lang-org · tech-adoption-curve-twenty-years