O que eu acho verdadeiramente digno de nota, em relação à utilização de provadores automáticos é que, na hora que a gente quer ter uma certeza de ter seguido todos e apenas os passos permitidos pelas regras formais, a gente tem que abrir mão de explicações intuitivas. Porque as intuições podem ser distorcidas, e dessa forma podem esconder algum passo em falso na construção de uma demonstração.
Então me parece meio que inevitável temos uma divisão em duas partes: a verificação de um resultado, em suas minúsculas formais, para em seguida ter uma apresentação mais intuitiva do resultado. Eu não estou querendo dizer que na prática é assim que os resultados surgem, pelo contrário. A demonstrações vem de intuições e ideias, que em seguida precisam ser validadas. Mas a gente está discutindo aqui a didática e não a pesquisa. []s On Wed, Jul 16, 2025 at 11:50 AM Joao Marcos <[email protected]> wrote: > Acrescento um comentário sobre "estas novidades que andam rolando por aí": > > > I wonder whether this (hermetic?) presentational style is experiencing a > resurgence > > with the rise of proof assistants, whose formal theories rarely > prioritize the > > communication of mathematical intuition. In this context, is > communication itself > > confined to peripheral commentary? > https://x.com/antitheorem/status/1945463475452441041 > > O que acham os colegas? > > []s, Joao Marcos > > On Mon, Jul 14, 2025 at 12:34 PM Joao Marcos <[email protected]> wrote: > >> "The desiccated "Theorem, Lemma, Proof, Corollary,..." presentational >> style is staggeringly counterproductive, if one's objective is >> actually communicating the underlying mathematical intuitions and >> thought processes behind a result." >> https://x.com/getjonwithit/status/1943232298977030348 >> >> Uma das grandes dificuldades que matemáticos em formação encontram ao >> entrar na guilda para aprender os ossos do ofício é que nesta área não >> é habitual contar a história de como se chegou a um certo resultado, e >> o costumeiro, na realidade, é esconder tudo que deu errado pelo >> caminho... >> >> Alguns ainda vão mais além, e acrescentam que é importante "motivar >> mais" os resultados teóricos e também se esforçar mais por >> familiarizar os estudantes com a "história da área". Tudo isto se >> aplica à Lógica, claro: o quão importante seria *para o aprendizado do >> neófito*, digamos, a ampla _motivação_ prática da introdução de certos >> métodos ou estratégias de raciocínio, ou a apresentação detalhada do >> _histórico_ de como certos conceitos foram paulatinamente >> desenvolvidos por estes ou aqueles gênios ou civilizações >> particulares? >> >> No geral, o que pensam os colegas sobre a forma clássica de exposição >> dos avanços matemáticos? >> >> []s, Joao Marcos >> > > > -- > https://sites.google.com/site/sequiturquodlibet/ > > -- > LOGICA-L > Lista acadêmica brasileira dos profissionais e estudantes da área de > Lógica <[email protected]> > --- > 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 [email protected]. > Para ver esta conversa, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhA81SDbxDWT8-Ri8b2%3D2gOR4yk_WPO9T-4M78R4xU6wQ%40mail.gmail.com > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhA81SDbxDWT8-Ri8b2%3D2gOR4yk_WPO9T-4M78R4xU6wQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- Marcelo Finger Departament of Computer Science, IME-USP http://www.ime.usp.br/~mfinger ORCID: https://orcid.org/0000-0002-1391-1175 ResearcherID: A-4670-2009 Instituto de Matemática e Estatística, Universidade de São Paulo Rua do Matão, 1010 - CEP 05508-090 - São Paulo, SP -- 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/CAGG7Aw1OV_Dy6JU5g0JoZHiPuOZvHeJt_2wXNNeEomsHvH9RnQ%40mail.gmail.com.
