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 https://youtu.be/bwKFcLaeD1A Está no Spotify, para quem quer apenas ouvir: https://open.spotify.com/episode/7wSSQuqMXCq69atlRKqYyO E nas demais plataformas de podcast: Apple: https://podcasts.apple.com/us/podcast/professor-adolfo-neto/id1490465804?uo=4 Google: https://podcasts.google.com/feed/aHR0cHM6Ly9hbmNob3IuZm0vcy8xMGYyYmE3NC9wb2RjYXN0L3Jzcw== 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 On Fri, Nov 19, 2021 at 10:01 AM Adolfo Neto <adolfo....@gmail.com> wrote: > 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." > https://www.nature.com/articles/d41586-021-01627-2 > > Aqui dois matemáticos que sinceramente não conheço falando sobre Lean > > https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ > https://www.ma.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf > > 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 > 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 > ================================================================== > -- ================================================================== 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 ================================================================== -- Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYVRJTrM%3D8Pz_1pRh7gZYcwjsZ5b7HuofwXwZ1nNSfJrXA%40mail.gmail.com.
