Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

11 views
Skip to first unread message

Joao Marcos

unread,
Jun 20, 2021, 6:39:58 AM6/20/21
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

Proof-assistant software handles an abstract concept at the cutting
edge of research, revealing a bigger role for software in mathematics.

-- Davide Castelvecchi
https://www.nature.com/articles/d41586-021-01627-2


JM

Walter Carnielli

unread,
Jun 20, 2021, 10:11:47 AM6/20/21
to Joao Marcos, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Para fazer alguma justiça- o artigo diz:

"Lean was originally created by a computer scientist at Microsoft Research in Redmond, Washington, for the purpose of rigorously checking computer code for bugs".

Não é  claro a quem  estão se referindo,  mas, a própria  página da "Community" informa:


"The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura at Microsoft Research".



Abs
W.

--
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+u...@dimap.ufrn.br.
Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjovD_XR2pOwj78Khgsrs_U9uLa3na9JZJba2HJ%3D82MKw%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages