Oi João,
Acho que se eu dividir a sua idéia em várias em consigo puxar a
sardinha pra brasa que me interessa.
Eu IMAGINO que agora as pessoas estejam publicando um monte de artigos
com teoremas cuja intuição é bem difícil de entender, e que ao invés
deles terem demonstrações horríveis feitas à mão como antigamente
esses artigos novos têm demonstrações horríveis feitas num proof
assistant... mas vamos pensar nas pessoas que têm teoremas
interessantes e que decidem que é melhor publicá-los em dois estilos
diferentes - uma versão longa no Arxiv, com a intuição, pra muita
gente ler, e uma versão enxutíssima num journal prestigioso que dá
muitos pontos de currículo. O que é a "intuição por trás do teorema"
pra essas pessoas? Em alguns casos são figuras, em outros casos são
certos casos particulares que motivaram o teorema mais geral...
algumas dessas pessoas devem estar procurando modos de mostrar essa
intuição, e algumas devem estar fazendo programas pra fazer as
figuras, ou até animações, de vários casos particulares - e outras
podem estar fazendo coisas ainda mais legais, como estender a
linguagem de alguns proof assistants pra eles "entenderem a linguagem
da versão intuitiva"...
CADÊ ESSAS PESSOAS?
[[]],
Eduardo
On Wed, 16 Jul 2025 at 11:50, 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>
> .
>
--
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/CADs%2B%2B6g0zkV_m1NRem2MEnOCJkMc3OT0jhiTW8y5RMMyqPLbdQ%40mail.gmail.com.
