PeopleofSuperintelligence

Researcher

Leo de Moura

Also known as Leonardo de Moura

Leo de Moura is a computer scientist whose work on theorem proving helps AI systems produce mathematical proofs that Lean checks. He studied in Brazil and began his career at SRI before joining Microsoft to build Z3. He started Lean in 2013 and coauthored papers on the Lean theorem prover and Lean 4. He joined the Artificial Intelligence Mathematical Olympiad Prize's advisory committee in 2024, and Lean received ACM SIGPLAN's Programming Languages Software Award in 2025. As of October 2026, he is a Senior Principal Applied Scientist at AWS and Chief Architect and co-founder of the Lean FRO.

Now at
Amazon and Lean Focused Research Organization
Works
91
Citations
12,771
h-index
39

Publication numbers from OpenAlex, as of 15 October 2026.

Timeline

  1. By 2006

    Studies in Brazil and early work

    By 2006, he completes his studies in Brazil at PUC in Rio de Janeiro and starts work on SRI's model checker as his first job.

  2. 2006–2013

    Building the Z3 solver

    Microsoft hires him in 2006 to build an SMT solver, and he leads the Z3 project through 2013.

  3. 2013

    Starting the Lean project

    In 2013, he begins developing Lean at Microsoft Research.

  4. 2015

    Describing Lean's prover

    In 2015, he coauthors The Lean Theorem Prover (System Description) with Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer.

  5. 2021

    Publishing Lean 4

    In 2021, he and Sebastian Ullrich coauthor The Lean 4 Theorem Prover and Programming Language.

  6. 2024

    The AIMO advisory committee

    In 2024, he joins the Artificial Intelligence Mathematical Olympiad Prize's advisory committee as Lean's Chief Architect.

  7. 2025

    An ACM award for Lean

    In 2025, ACM SIGPLAN recognizes Lean with its Programming Languages Software Award and lists de Moura among four contributors. Lean serves as a de facto choice for AI-based systems of mathematical reasoning.

  8. As of October 2026

    Leading Lean FRO

    As of October 2026, he is a Senior Principal Applied Scientist at AWS and Chief Architect and Co-Founder of the Lean FRO. In August 2026, his lecture shows how AI writes proofs that Lean's kernel checks.

Sources and credits

Photo: We have no published photo of Leo de Moura yet. Send us a free-licensed photo.

  1. From SMT Solvers to Lean and the Future of Automated Reasoning etaps.org. Checked 15 October 2026.
  2. Lean - Microsoft Research: Publications microsoft.com. Checked 15 October 2026.
  3. AIMO Prize Appoints Further Advisory Committee Members aimoprize.com. Checked 15 October 2026.
  4. Programming Languages Software Award sigplan-pages.sigplan.hosting.acm.org. Checked 15 October 2026.
  5. Software Verification in Lean leodemoura.github.io. Checked 15 October 2026.
  6. Team — Lean Lang lean-lang.org. Checked 15 October 2026.