DEV Community

Elixir UTFPR (por Adolfo Neto)
Elixir UTFPR (por Adolfo Neto)

Posted on

2

Raciocínio Automatizado com Leonardo de Moura, Pesquisador na Microsoft Research

Acabei de entrevistar Leonardo de Moura.

A entrevista está no Spotify, para quem quer apenas ouvir: https://open.spotify.com/episode/7wSSQuqMXCq69atlRKqYyO

O Anchor contém links para diversos outros aplicativos de podcasts: https://anchor.fm/adolfont/episodes/Raciocnio-Automatizado-com-Leonardo-de-Moura--Pesquisador-na-Microsoft-Research-e1anc8j

Leonardo de Moura é um brasileiro que trabalha na Microsoft Research. Ele é um pesquisador bastante citado. Leonardo publicou o artigo Z3: An efficient SMT solver em 2008. Verifiquei hoje (23/11/2021) e o artigo já tem mais de 7900 citações, 937 só no ano passado!

Leonardo de Moura criou o provador de teoremas Z3 e o assistente de provas Lean que, na sua versão 4, é também uma linguagem de programação funcional.

Como não encontrei nenhuma entrevista ou palestra dele gravada em português no YouTube, decidi eu mesmo fazâ-la. Em inglês há esta palestra dele explicando o Lean 4, entre outras.

Image of Timescale

🚀 pgai Vectorizer: SQLAlchemy and LiteLLM Make Vector Search Simple

We built pgai Vectorizer to simplify embedding management for AI applications—without needing a separate database or complex infrastructure. Since launch, developers have created over 3,000 vectorizers on Timescale Cloud, with many more self-hosted.

Read full post →

Top comments (0)

Image of Docusign

🛠️ Bring your solution into Docusign. Reach over 1.6M customers.

Docusign is now extensible. Overcome challenges with disconnected products and inaccessible data by bringing your solutions into Docusign and publishing to 1.6M customers in the App Center.

Learn more