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 ================================================================== -- 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/CANspyYX-4j%2BxQ3x5fhHnKzBgcMTOzq2FXf-dPZzaEawCGaw1yQ%40mail.gmail.com.
