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 <adolfo....@gmail.com> escreveu: > > 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ê 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+unsubscr...@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.carnie...@cle.unicamp.br Website: http://www.cle.unicamp.br/prof/carnielli -- 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/CAOrCsLfy%3D6oHaE%3DAjEPxUBU2UapigboGnbQM2wzRnW2baQfYcw%40mail.gmail.com.
