Entrevista com Leonardo de Moura (Microsoft Research)
107 views
Skip to first unread message
Adolfo Neto
Nov 19, 2021, 8:02:16 AM11/19/21
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Oi pessoal,
Nesta terça à tarde vou entrevistar o Leonardo de Moura, da Microsoft Research https://leodemoura.github.io/.
Ele é criador do Lean Prover, um provador de teoremas interativo que é também uma linguagem de programação funcional: https://leanprover.github.io/about/
O Lean saiu até na Nature:
"For help checking that work, Scholze turned to Buzzard, a fellow number theorist who is an expert in Lean, a proof-assistant software package. Lean was originally created by a computer scientist at Microsoft Research in Redmond, Washington, for the purpose of rigorously checking computer code for bugs."
Aqui dois matemáticos que sinceramente não conheço falando sobre Lean
Leonardo fez Doutorado na PUC-Rio, orientado por Carlos Lucena e co-orientador pelo Hermann.
Se alguém tiver alguma pergunta que queira que eu faça a ele, é só responder a este email. Agradeço a ajuda e mencionarei seu nome (se assim o quiser).
Abs.
Adolfo
==================================================================
Adolfo Neto
Adolfo Neto
Associate Professor - Federal University of Technology, Paraná
Web: http://www.dainf.ct.utfpr.edu.br/~adolfo
Mestrado em Computação Aplicada: http://www.ppgca.ct.utfpr.edu.br
==================================================================
Mestrado em Computação Aplicada: http://www.ppgca.ct.utfpr.edu.br
==================================================================
Walter Carnielli
Nov 19, 2021, 11:40:22 AM11/19/21
to Adolfo Neto, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Ola Adolfo,
Vou te enviar uma pergunta em privado, assim você pode decidir
livremente se usa ou nao : -)
Kevin Buzzard é um matemático do Imperial College, especialista em
teoria dos números algébricos, usa e sabe muito sobre LEAN. Ele deu
uma live recentemente (eu até discuti um pouco com ele sobre a
prova da versão paraconsistente dos Teoremas de Goedel que David
Fuenmayor e eu propusemos usando Isabelle). Thomas Hales foi quem
demonstrou, com Samuel Ferguson, a conjectura de Kepler sobre a
densidade do empilhamento de esferas em 1989.
Kepler conjecturou há 300 anos que a melhor maneira seria como se
empilham laranjas no mercado, e de fato é ,cmas a prova ficou anos
esperando aprovação Em 2014 Hales anunciou a conclusão do Projeto
Flyspeck, que verificou formalmente a corretude de sua própria prova
da conjectura de Kepler usando HOL Light.
Abs
Walter
Em sex., 19 de nov. de 2021 às 10:02, Adolfo Neto
<adolf...@gmail.com> escreveu:
> --
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYX-4j%2BxQ3x5fhHnKzBgcMTOzq2FXf-dPZzaEawCGaw1yQ%40mail.gmail.com.
--
===========================
Walter Carnielli, Professor
Centre for Logic, Epistemology and the History of Science and
Department of Philosophy
University of Campinas –UNICAMP
13083-859 Campinas -SP, Brazil
Phone: (+55) (19) 3521-6517
Institutional e-mail: walter.c...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli
Vou te enviar uma pergunta em privado, assim você pode decidir
livremente se usa ou nao : -)
Kevin Buzzard é um matemático do Imperial College, especialista em
teoria dos números algébricos, usa e sabe muito sobre LEAN. Ele deu
uma live recentemente (eu até discuti um pouco com ele sobre a
prova da versão paraconsistente dos Teoremas de Goedel que David
Fuenmayor e eu propusemos usando Isabelle). Thomas Hales foi quem
demonstrou, com Samuel Ferguson, a conjectura de Kepler sobre a
densidade do empilhamento de esferas em 1989.
Kepler conjecturou há 300 anos que a melhor maneira seria como se
empilham laranjas no mercado, e de fato é ,cmas a prova ficou anos
esperando aprovação Em 2014 Hales anunciou a conclusão do Projeto
Flyspeck, que verificou formalmente a corretude de sua própria prova
da conjectura de Kepler usando HOL Light.
Abs
Walter
Em sex., 19 de nov. de 2021 às 10:02, Adolfo Neto
<adolf...@gmail.com> escreveu:
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYX-4j%2BxQ3x5fhHnKzBgcMTOzq2FXf-dPZzaEawCGaw1yQ%40mail.gmail.com.
--
===========================
Walter Carnielli, Professor
Centre for Logic, Epistemology and the History of Science and
Department of Philosophy
University of Campinas –UNICAMP
13083-859 Campinas -SP, Brazil
Phone: (+55) (19) 3521-6517
Institutional e-mail: walter.c...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli
Adolfo Neto
Nov 23, 2021, 3:03:25 PM11/23/21
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Olá a todos/todas/todes,
A entrevista com o Leonardo foi ótima. Agradeço o interesse e a ajuda de alguns com perguntas.
Ela está no YouTube, para quem prefere ver e ouvir:
Raciocínio Automatizado com Leonardo de Moura, Pesquisador na Microsoft Research
Está no Spotify, para quem quer apenas ouvir: https://open.spotify.com/episode/7wSSQuqMXCq69atlRKqYyO
E nas demais plataformas de podcast:
No Anchor que 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
Em alguns casos, dependendo do aplicativo, pode demorar ainda algumas horas para chegar no seu app de podcasts.
Abs.
Adolfo
Adolfo
Reply all
Reply to author
Forward
0 new messages