Progresso da formalização do Último Teorema de Fermat
(xenaproject.wordpress.com)- O trabalho de portar a prova do FLT para o Lean está em andamento há dois meses; as definições de R e T necessárias para o teorema “R=T” de Wiles ainda não foram concluídas, mas um resultado de álgebra comutativa abstrata já foi provado
- O objetivo não é reproduzir exatamente a prova original dos anos 1990, mas construir sobre Lean e mathlib uma prova generalizada e simplificada com base em trabalhos posteriores de Diamond/Fujiwara, Kisin, Taylor, Scholze e outros
- Durante a formalização da cohomologia cristalina necessária para a prova moderna, surgiu um problema: um lema auxiliar central no artigo de 1965 de Roby, referência padrão para estruturas de divided powers, parece estar incorreto
- Brian Conrad encontrou uma prova alternativa no apêndice do livro de Berthelot-Ogus, e Arthur Ogus também respondeu que sabe como corrigir os erros desse apêndice, permitindo que o projeto avance novamente
- Este caso mostra o risco de detalhes da matemática moderna dependerem da memória de especialistas e de conhecimento tácito, reforçando motivos práticos para registrar provas em sistemas formais
Estado atual da migração da prova do FLT para Lean
- O trabalho de ensinar ao computador a prova do Último Teorema de Fermat (FLT) está em andamento há dois meses
- No teorema “R=T”, ponto central da prova de Wiles, é necessário muito trabalho para definir em Lean o que são R e T, e ambas as definições ainda não estão concluídas
- O doutorando Andrew Yang já provou um resultado necessário de álgebra comutativa abstrata
- Trata-se de um resultado do tipo: “se anéis abstratos R e T satisfazem várias condições técnicas, então são iguais”
- A versão atual está publicada como blueprint
- O sistema usado é o Lean e a biblioteca matemática mathlib
- Quem conhece um pouco de Lean e teoria dos números pode participar por meio das contribution guidelines, do project dashboard e das issues
Por que não portar literalmente a prova dos anos 1990
- O projeto não formaliza exatamente a prova de Wiles dos anos 1990
- Depois disso, trabalhos de Diamond/Fujiwara, Kisin, Taylor, Scholze e outros tornaram a prova mais geral e mais simples
- O objetivo não é apenas provar o FLT, mas construir dentro do Lean resultados mais gerais e mais poderosos
- Se a revolução da matemática por IA realmente acontecer e o Lean se tornar um componente importante, pode ser útil que o computador tenha definições centrais da teoria moderna dos números em uma forma compreensível
Divided powers necessárias para a cohomologia cristalina
- A prova que se quer formalizar usa cohomologia cristalina, ausente da prova original de Wiles
- Essa teoria foi desenvolvida em Paris nas décadas de 1960 e 1970, e Berthelot estabeleceu seus fundamentos com base em ideias de Grothendieck
- As funções exponencial e logaritmo clássicas são importantes para entender geometria diferencial e cohomologia de de Rham, mas não funcionam da mesma forma em contextos aritméticos como characteristic p
- As estruturas de divided powers, desenvolvidas em artigos de Roby nos anos 1960, desempenham papel central na construção de funções análogas utilizáveis em contextos aritméticos
- Para ensinar cohomologia cristalina ao Lean, primeiro é preciso formalizar divided powers
O problema na literatura de Roby revelado durante o trabalho em Lean
- Antoine Chambert-Loir e Maria Ines de Frutos Fernandez estavam formalizando em Lean a teoria de divided powers
- Durante o verão, o Lean revelou um problema na argumentação humana da literatura padrão e, após verificação, um lema auxiliar central do trabalho de Roby pareceu estar incorreto
- Tecnicamente, o artigo de Berthelot não desenvolve a teoria de divided powers desde o início, mas usa “Les algebres a puissances divisees”, de Roby
- O artigo foi publicado em Bull Sci Math, 2ième série, 89, 1965, p. 75-91
- O Lemme 8 na p. 86 parece ser falso, e não estava claro como corrigir sua prova
- A prova cita incorretamente outro lema do artigo de 1963 de Roby na Ann Sci ENS
- A proposição correta é
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R), mas na aplicação faltou um tensor product
- Esse problema quebra a prova de Roby de que a álgebra de divided powers de um módulo possui divided powers e, como consequência, impedia a definição do anel
A_cris
Mais próximo de “a prova está vazia” do que de “a teoria está errada”
- Isso não significa que a cohomologia cristalina em si esteja substancialmente errada
- Os principais teoremas ainda parecem corretos, mas a prova seguida por Antoine e Maria Ines era incompleta
- Roby, Grothendieck e Berthelot já faleceram, portanto não era possível consultar diretamente os especialistas originais
- Vários especialistas consideram que, mesmo se um lema intermediário for falso, a prova dos resultados principais ainda pode ser corrigida
- Na formalização, porém, não basta achar que “deve dar para corrigir”; é preciso ter a prova corrigida de fato
O apêndice de Berthelot-Ogus abriu um desvio
- Tadashi Tokieda contou essa história a Brian Conrad em Stanford, e Conrad perguntou o que significava dizer que a cohomologia cristalina estava errada
- Após ouvir os detalhes técnicos, Conrad concordou que parecia haver um problema e passou a examinar o caso
- Algumas horas depois, Conrad informou que no apêndice do livro de Berthelot-Ogus sobre cohomologia cristalina havia uma prova diferente de que a universal divided power algebra of a module possui divided powers
- Na visão de Conrad, essa abordagem parecia funcionar bem, e graças a isso a prova pôde voltar a avançar
- Depois, durante um almoço com Arthur Ogus em Berkeley, ao ouvir que esse apêndice resolvia o problema, Ogus respondeu que o próprio apêndice também contém vários erros, mas que ele sabe como corrigi-los
Por que a literatura matemática moderna precisa de formalização
- Esse processo mostrou que a forma como humanos documentam a matemática moderna talvez não seja robusta o suficiente
- Muitos fatos permanecem como algo que “os especialistas sabem”, sem estarem organizados com precisão na literatura
- Mesmo que as ideias importantes sejam robustas o bastante para resistir a esse tipo de choque, os detalhes efetivos das provas podem não estar onde se esperava
- Registrar corretamente a matemática em sistemas formais pode reduzir muito a possibilidade de erro
- Mesmo para matemáticos que não são formalistas, se quisermos que máquinas aprendam argumentos humanos e façam matemática por conta própria, primeiro será preciso ensinar esses argumentos às máquinas
- Maria Ines apresentou a formalização de divided powers no seminário Cambridge Formalization of Mathematics em uma palestra, e entende-se que esses problemas foram organizados
- O projeto voltou aos trilhos, mas continua existindo a possibilidade de a literatura causar novos bloqueios
1 comentários
Opiniões do Hacker News
Lembro de quando, na pós-graduação, eu escrevia código rápido para ajudar na abordagem computacional do meu orientador para a conjectura de Birch–Swinnerton-Dyer
Em um seminário de teoria dos números numa cidade próxima, me perguntaram se eu estava “tentando reforçar as evidências que sustentavam a conjectura”, e respondi, rindo: “Não, na verdade eu queria encontrar um contraexemplo”; os especialistas ficaram muito irritados
A teoria dos números é tão antiga e profunda que escrever uma tese de doutorado na área é quase o primeiro passo para virar iniciante; eu conhecia a notação e as definições, mas não alcançava a intuição por baixo delas
Por isso, a raiva que os especialistas demonstraram quando eu disse que “esperava um contraexemplo” me deixou mais curioso do que assustado, e fiquei me perguntando o que eles estavam vendo, mas ainda não conseguiam expressar em palavras
Esse tipo de avanço na formalização torna a matemática muito mais acessível para quem está mais acostumado com programação
A ansiedade quanto à falta de formalidade é legítima, mas acho que a resposta correta à ansiedade não é a evitação, e sim a curiosidade
Se um novato inexperiente como você encontrasse um contraexemplo com cálculos grosseiros e ficasse famoso da noite para o dia, todo esse esforço e essa estrutura poderiam desmoronar; imagino que por isso tenham ficado irritados
Se eu fosse dar um conselho ao meu eu jovem na pós-graduação em matemática, diria para gastar pelo menos 1/4 do tempo de cada tarefa não trivial do tipo “prove X” procurando contraexemplos
Em exercícios, você vai fracassar 99% das vezes, mas sua compreensão do problema será muito maior; no 1% restante, pode parecer um gênio
Quando você entra na pesquisa matemática de fato, essa probabilidade muda de forma muito mais favorável para a abordagem de buscar contraexemplos primeiro
Lembro que, quando eu era estudante, um amigo me contou que alguém tinha terminado o primeiro dia de um seminário e todos estavam empolgados, dizendo que ele iria provar o último teorema de Fermat
Essa pessoa era Andrew Wiles e, depois, após alguns meses corrigindo um problema descoberto antes da publicação, finalmente tudo foi publicado
Para quem estudava matemática, foi um acontecimento incrivelmente empolgante; por isso, quando vejo a expressão “prova antiquada dos anos 1990”, eu realmente me sinto velho
Quase toda a turma era de alunos de pós-graduação em matemática, e acho que eu não entendi nem 20% do material
Gostei da parte em que o Lean fez algo irritante que ele às vezes faz: reclamou da apresentação, em estilo humano, de um argumento na literatura padrão, e, olhando com atenção, havia de fato uma lacuna no argumento humano
Tirando a irritação meio em tom de brincadeira, isso é algo extraordinário, e acho que o Lean e outros provadores de teoremas se tornarão ferramentas importantes na matemática
A parte sobre a documentação ruim da matemática moderna me parece parecida com UI/UX/design web
Um designer cria mockups, protótipos e fluxos de interação informais e imprecisos e os entrega ao desenvolvedor; então o desenvolvedor precisa formalizar aquilo em código e explicar com precisão à máquina
Nesse processo, inevitavelmente encontra buracos, como cenários de interação ou caminhos de código que o projeto não considerou, e às vezes surgem grandes falhas de design que o desenvolvedor ou o designer precisa preencher
Design e desenvolvimento são papéis diferentes e exigem modos de pensar diferentes, e a maioria dos designers resiste bastante a trabalhar e pensar como desenvolvedores
Depois desse fracasso, aprendemos que não é possível formalizar completamente a matemática, e isso aponta para o problema fundamental da abordagem de tentar fazer matemática com IA
Se você se interessa por esse tema, vale a pena olhar o código de verdade
Ex.: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
Também vale ver o blueprint que explica a estrutura geral do código: https://imperialcollegelondon.github.io/FLT/blueprint/
Como alguém olhando de fora, é muito interessante ver como é o código Lean e como as pessoas contribuem
Também gosto do fato de não precisar de testes unitários. Em certo sentido, a proposição final da prova é o teste unitário
Por exemplo, exemplos triviais e contraexemplos para verificar que uma definição não é vazia cumprem esse papel
Do ponto de vista de alguém que trabalhou com matemática pura, o grande problema é que os matemáticos quase nunca fornecem provas autocontidas
Não há incentivo para isso, e às vezes os autores até se orgulham de “omitir detalhes”
No fim, se você quer uma prova rigorosa em que seja possível acompanhar todos os passos lógicos, um especialista precisa preencher lacunas que não são fáceis de encontrar na literatura
Às vezes isso só se torna possível quando essa pessoa escreve um livro explicando tudo, e mesmo assim, em alguns casos, nem isso basta
Considerando apenas o que está registrado, boa parte da matemática moderna está sobre uma base instável
Artigos de pesquisa em matemática são escritos para outros especialistas da área, e às vezes há detalhes de menos, algo de que frequentemente reclamamos na revisão por pares
Mas, se todos os detalhes fossem realmente fornecidos, os artigos ficariam muito mais longos
Como exemplo que alguém com uma base sólida de matemática do ensino médio conseguiria resolver, há o problema de provar que existem constantes C, X > 0 tais que, para algum real x > X,
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < CxProposições desse tipo aparecem o tempo todo em teoria analítica dos números e, para especialistas, são óbvias, então quase sempre são escritas nos artigos sem prova
Produzir uma prova completa e rigorosa seria longo e sem graça, e nenhum especialista iria querer lê-la
Há um custo de compromisso nessa postura, mas ele parece administrável
Isso soa como a terceira etapa mencionada por Tao: intuição informada
Ele dizia: “se você já fez algo 100 vezes, pode simplesmente dizer ‘como se observa facilmente’ e seguir em frente”
Pelo que entendi, seria como uma pessoa com uma base de dados na cabeça fazendo o trabalho de identificar se as precondições de um teorema e a conclusão da frase seguinte batem
Ou será que existe matemática que, hoje, não pode ser expressa de uma forma que os verificadores de provas consigam avaliar?
Ou talvez o uso de verificadores de provas simplesmente não seja tão difundido quanto eu imaginava. Soa parecido com a posição das linguagens de tipagem estática na programação
Ou seja, se já houve uma prova amplamente aceita com uma falha fatal por causa de uma parte tratada no “aceno de mãos”
Se isso não aconteceu, dá para entender por que há uma postura mais relaxada em explicitar os detalhes
Sempre me perguntei se a intuição de que “a cohomology crystalline tem sido usada tanto desde os anos 1970 que, se houvesse um problema, ele já teria aparecido há muito tempo” é realmente correta
Será que é mesmo tão impossível uma área inteira da matemática se desenvolver sobre uma prova defeituosa e simplesmente acabar se revelando falsa?
Ele viu pessoalmente uma área ruir por causa de um erro no “primeiro lema da primeira página” de um artigo fundamental
Dá para dizer que o trabalho inicial no UniMath, o ano especial no IAS e depois o livro de HoTT foram o fluxo que elevou o tema da formalização da matemática à posição que ocupa hoje
Se a base estiver errada, um desses contraexemplos também pode refutar um teorema fundamental, então construir sobre uma base incorreta tende, na verdade, a revelar os defeitos dessa base
De modo parecido, quando a matemática é às vezes aplicada para produzir previsões, se a matemática estiver errada, as previsões também estarão, e essas previsões erradas atraem muita atenção
Na verdade, a palavra “área” é um pouco enganosa; muitas teorias são mais como nós ligados a várias outras teorias por toda a matemática
Essas teorias, por sua vez, se conectam a outras teorias
Seria uma situação muito estranha se apenas a base ruísse logicamente sem nenhum efeito sobre outras partes desse nó
Um enorme pedaço flutuante de matemática, internamente totalmente consistente mas com um único erro, é difícil de imaginar no caso de cohomology deste texto
A rigor, isso é mais uma atitude filosófica, mas quero acreditar que boa parte da matemática atual foi, em certo sentido, descoberta naturalmente
Spoiler: mesmo assim, o mundo continuou girando
Ao longo do último ano, tentei de forma intermitente formalizar em Lean parte de um curso de graduação de análise complexa
Aprendi muito e foi gratificante, mas às vezes também foi frustrante
Só recentemente consegui definir por completo a forma polar como uma bijeção de C* para (-pi,pi] x R, porque insisti em defini-la “do zero”, embora números complexos, séries de potências, exp e sin já existam na mathlib
É bem possível que boa parte da dificuldade tenha vindo do fato de eu ter apenas bacharelado em matemática, não estar familiarizado com Lean/mathlib e não ter alguém para me orientar. Ainda assim, a comunidade no Zulip foi extremamente útil
Muitos resultados da mathlib são formulados de maneira bastante abstrata, o que dificulta entender como eles se conectam a teoremas-padrão de graduação, ou mesmo se esses teoremas estão na mathlib
Isso faz sentido para a comunidade de pesquisa em matemática, mas, para mim pessoalmente, foi um grande obstáculo; e, se Lean vier a ser mais usado no ensino, pode se tornar um problema semelhante. Ainda assim, é algo que pode ser organizado com o tempo
Na minha opinião, a automação de provas ainda não é suficiente
Coisas demais são mais difíceis de provar do que deveriam ser, e em especial as conversões de tipo são o que mais me incomoda
Na matemática usual, os reais são um subconjunto dos complexos, então tudo que é verdadeiro para todos os complexos é automaticamente verdadeiro para todos os reais; em Lean, porém, eles são tipos diferentes, e é preciso ir de um para o outro por meio de mapas injetivos/operações de conversão de tipo, o que obscurece o ponto central da prova
Quando conversões de tipo se acumulam, como transformar naturais em reais e depois em complexos, fica especialmente bagunçado
Claro que isso pode ser um problema específico do tema; em áreas como álgebra, que lidam com mapas explícitos, imagino que pareça muito mais natural
É muito fácil receber orientação sobre como usar a mathlib, o que existe e onde encontrar
Problemas com camadas de conversões de tipo geralmente são resolvidos com a tática
norm_castMesmo que não seja uma pergunta específica, se você mencionar de passagem ou mostrar no código um estilo de prova desnecessariamente complicado, pode receber sugestões de táticas que não conhecia
Se você só tem a sensação de que a formalização está difícil demais e não sabe que técnica usar, pode isolar uma prova insatisfatória que deu trabalho para montar e perguntar para as pessoas tentarem reduzi-la
Esse tipo de pergunta normalmente é bem recebido, e todo mundo aprende bastante
Esta thread parece ser sobre como escrever bem matemática
Passei décadas lendo, escrevendo, ensinando, aplicando e publicando matemática, e também recebi um doutorado em matemática aplicada
É verdade que há problemas na escrita matemática, e parte da matemática é escrita de forma péssima
Mas também existe matemática muito bem escrita
No mínimo, todos os símbolos devem ser definidos antes de serem usados; ajuda dar motivação antes de apresentar a matemática; e, às vezes, explicações intuitivas também são úteis
Ler com atenção matemática bem escrita ajuda a aprender escrita matemática
Exemplos incluem Finite-Dimensional Vector Spaces, de Paul R. Halmos; Advanced Calculus, de R. Creighton Buck; Mathematical Analysis, de Tom M. Apostol; Real Analysis, de H. L. Royden; Real and Complex Analysis, de Walter Rudin; Probability, de Leo Breiman; e Mathematical Foundations of the Calculus of Probability, de Jacques Neveu
O autor tentou verificar o Último Teorema de Fermat exatamente da forma como ele foi desenvolvido na literatura e, no processo, descobriu que um lema que sustentava uma subárea não era verdadeiro na forma em que era usado
Ainda assim, o motivo para acreditar que a área é em grande parte recuperável é a confiança de que, se ela estivesse realmente errada, alguém já teria encontrado um resultado negativo
Agora era preciso encontrar um substituto adequado para sustentar essa área
O autor escreve de um jeito bastante divertido; foi uma experiência curiosa, porque foi fácil de ler mesmo eu não tendo entendido cerca de metade
Encontrei vitiated como uma boa palavra para usar quando uma prova é refutada ou se descobre que ela tem uma falha
Gosto dela porque passa a ideia de que a prova foi danificada e precisa de uma nova prova ou de reparo, sem sugerir tanto o mal-entendido de que a conclusão foi provada falsa