Leonardo de Moura

Biografia

Alma mater	Pontifícia Universidade Católica do Rio de Janeiro
Orientador(a)(es/s)	Carlos José Pereira de Lucena Edward Hermann Haeusler (d)
Atividades	cientista de computação matemático

Outras informações

Empregador	Microsoft Research (2006-2023) Amazon Web Services (a partir de 2023)
Orientador de doutorado	Carlos José Pereira de Lucena Edward Hermann Haeusler (d)
Website	(en) leodemoura.github.io
Distinção	Prêmio Herbrand (2019)

'Magnum opus'

Lean Z3 Theorem Prover (d) Yices (d)

editar - editar código-fonte - editar Wikidata

Leonardo de Moura é um cientista da computação e criador do ^[1] Lean, uma ferramenta de raciocínio automatizado utilizada como assistente de provas matemáticas, escrito na época em que trabalhou na Microsoft Research.^[2] Atualmente, trabalha na AWS e é Chief Architect da Lean FRO.^[3] Graduado em engenharia pela PUC-RJ, fez mestrado e doutorado em Ciência da Computação na mesma instituição.^[4]

Prêmios e Honrarias

• O Prêmio CADE Skolem de 2007 pelo artigo "Eficiente E-Matching para SMT Solvers" que passou o teste do tempo, por ser um artigo mais influente no campo.^[5]
• O Prêmio de Verificação Assistida por Computador de 2021 pelas contribuições que mudaram o campo em relação ao seu trabalho em Z3.^[6]
• O prémio CADE Skolem de 2025 pelo artigo "The Lean Theorem Prover (System Description) " que passou o teste do tempo, por ser um artigo mais influente no campo.^[5]
• O Prêmio de Software de Línguas de Programação ACM SIGPLAN de 2025 por seu trabalho em Lean.^[7]

Referências