"curiosamente, não há menção a assistentes de demonstração --- ou mesmo à Teoria das Demonstrações"
Não acho isso nem mesmo muito curioso. Marcelo Viana evita dar qualquer protagonismo à lógica, nem menciona que o LEAN é construído com teoria dos tipos dependentes, nem que isso é um assunto basicamente da Lógica. Não vai se referir à teoria das demonstrações (ou teoria da prova), e nem reconhecer que um tópico eminentemente lógico poderá ser muito influente nos fundamentos de toda a matemática. ( vamos ver o resto das fatias, até agora temos três. .) Abs Walter ======================== Walter Carnielli CLE and Department of Philosophy University of Campinas –UNICAMP, Brazil AI2- Advanced Institute for Artificial Intelligence Blog https://waltercarnielli.com/ Em qua., 8 de abr. de 2026 15:08, Joao Marcos <[email protected]> escreveu: > "Como sabemos se a prova de um teorema está certa?" > --- por Marcelo Viana > > https://www1.folha.uol.com.br/colunas/marceloviana/2026/04/como-sabemos-se-a-prova-de-um-teorema-esta-certa.shtml > > (curiosamente, não há menção a assistentes de demonstração --- ou > mesmo à Teoria das Demonstrações) > > > JM > > -- > LOGICA-L > Lista acadêmica brasileira dos profissionais e estudantes da área de > Lógica <[email protected]> > --- > 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 [email protected]. > Para ver esta conversa, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjyjqWhum4HEaSU7wSuRjrwkQ3qrV3vfdQJWAxji%2BWh3Q%40mail.gmail.com > . > -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <[email protected]> --- 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 [email protected]. Para ver esta conversa, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAOrCsLcUo_M4i_pwVBNow38zvB7ETjKFRV70yDE4fMG9vETyTA%40mail.gmail.com.
