Aqui está uma pergunta importante com a qual devemos lidar cada vez mais à medida que os pipelines de IA para Matemática se tornam mais comuns: Por que nos importamos em resolver problemas difíceis? Quase sempre, a resposta *não* é porque queremos particularmente que o problema difícil seja resolvido. (1/12)

Questões como a existência de soluções globalmente suaves para as equações de Navier-Stokes são de interesse matemático não porque a resposta em si seja terrivelmente importante, mas porque temos razões para acreditar que o processo de *descobrir* a resposta é muito provável... (2/12)

...para proporcionar novas e profundas percepções sobre análise, PDEs, dinâmica de fluidos, etc., com novas técnicas a explorar. Resolver o teorema de Fermat deu-nos (indiretamente) o programa de Langlands. Resolver o teorema de Poincaré deu-nos o fluxo de Ricci. Espera-se que resolver as equações de Navier-Stokes nos dê algo igualmente monumental. (3/12)

De fato, identificamos tais problemas como sendo "interessantemente difíceis" precisamente porque intuimos que representam uma "lacuna" na nossa compreensão e métodos atuais. É por isso que os malucos que afirmam resolver (digamos) a hipótese de Riemann usando "truques" ou métodos elementares... (4/12)

...estão de certa forma a perder o foco: se um desses grandes problemas se revelasse solucionável apenas com os conhecimentos matemáticos e a tecnologia existentes, seria uma imensa decepção: uma fonte que pensávamos estar a jorrar está, na verdade, seca. (5/12)

O que isso tem a ver com AI? Bem, se alguém aceita a premissa de que problemas difíceis são principalmente interessantes por causa das novas percepções e entendimentos que eles proporcionam, isso levanta a questão (à luz dos desenvolvimentos em AI): quem é responsável pela parte do "entendimento"? (6/12)

Considere provas por exaustão (como no teorema das quatro cores), que há muito são consideradas algo controversas, porque fornecem a parte da "certeza epistémica" de uma prova, sem necessariamente fornecer qualquer uma da parte da "intuição" (que é geralmente o que nos importa) (7/12)

Assim, as provas por exaustão certamente não são "erradas", mas são, de certa forma, "enganadoras", ou talvez "autossabotadoras": elas encerram um problema potencialmente frutífero, enquanto elidem precisamente aqueles aspectos da matemática que a tornam interessante e valiosa de se fazer. (8/12)

Acho que as provas geradas por IA, na ausência de qualquer nível de compreensão ou insight por parte do humano que as gerou, devem ser consideradas de maneira muito semelhante. Se você gera automaticamente uma prova Lean de um grande teorema, isso é ótimo! Mas por que você fez isso? (9/12)

Se você não entender os novos insights/métodos que a prova contém, então tudo o que você fez foi transferir o fardo intelectual de si mesmo para quem estiver disposto a ler e entendê-lo (e, esperançosamente, comunicar os insights contidos nele a outros). (10/12)

A matemática é, em última análise, um artefato cultural humano (provavelmente o mais profundo, rico e antigo que temos). Resolver problemas difíceis sempre foi suposto ser um *proxy* para expandir esse artefato. A IA está tornando excitantemente fácil gerar novos caminhos de compreensão matemática.. (11/12)

...dentro desse artefato, mas também está a tornar mais fácil do que nunca alcançar o proxy (ou seja, resolver problemas difíceis), enquanto perde toda a razão pela qual nos importávamos em primeiro lugar (ou seja, aprofundar a nossa compreensão). Por favor, não faças isso. (12/12)