-
Projeto Xena e o Último Teorema de Fermat
- O projeto Xena tem como objetivo formalizar a matemática no computador. Isso visa permitir que, caso ocorra uma revolução da IA na matemática, os computadores possam ajudar a expandir as fronteiras da teoria dos números moderna.
-
Formalização do Último Teorema de Fermat
- Está em andamento o trabalho de provar o Último Teorema de Fermat (FLT) no computador. Nesse processo, o principal desafio é ensinar o teorema R=T ao computador.
- Em vez da prova original de Wiles, pretende-se formalizar uma prova moderna, generalizada e simplificada.
-
Cohomologia cristalina e estruturas de potências divididas
- A cohomologia cristalina é uma teoria desenvolvida nas décadas de 1960 e 1970 e desempenha um papel importante na formalização matemática.
- As estruturas de potências divididas são um conceito necessário para ensinar cohomologia cristalina ao computador.
-
O problema da documentação matemática humana
- Fica evidente a imprecisão da documentação matemática. Embora isso seja conhecido entre especialistas, muitas vezes a documentação não é feita adequadamente.
- O trabalho de formalização pode ajudar a resolver esses problemas.
-
A importância da formalização
- Formalizar a matemática é uma etapa importante para permitir que máquinas realizem raciocínios matemáticos por conta própria.
- Muitos matemáticos não sentem a necessidade da formalização, mas ela é essencial para reduzir erros humanos.
-
Conclusão
- Em uma apresentação recente, o problema da formalização das potências divididas foi resolvido. Isso significa que o projeto voltou aos trilhos.
1 comentários
Comentários do Hacker News
Recorda a experiência de escrever código rápido durante a pós-graduação para ajudar na conjectura de Birch e Swinnerton-Dyer. Quando disse em um seminário que queria encontrar um contraexemplo, os especialistas ficaram irritados. Não entendia a profundidade da matemática, mas ficou com a curiosidade despertada.
Sente alegria com o avanço do formalismo na matemática. Como programador, isso torna a matemática mais acessível. A ansiedade diante da falta de formalismo deve ser enfrentada com curiosidade.
Matemáticos frequentemente tendem a omitir detalhes. Se alguém quiser uma prova rigorosa, precisa da ajuda de especialistas. A matemática moderna está sobre bases instáveis.
Recorda o processo pelo qual Andrew Wiles provou o FLT. O modo de provar dos anos 1990 parece antigo.
Enfatiza a falta de documentação na matemática moderna. É preciso reduzir erros por meio de sistemas formais. Ensinar argumentos matemáticos às máquinas é importante.
Explica a diferença de papéis entre designers de UI/UX e desenvolvedores. Design e desenvolvimento exigem formas de pensar diferentes.
Espera que provadores de teoremas como o Lean se tornem ferramentas importantes na matemática.
Achar interessante examinar código em Lean. A declaração final da prova funciona como um teste unitário.
Levanta a dúvida sobre a possibilidade de conceitos matemáticos usados há décadas estarem errados.
Apresenta a palavra
vitiated, mencionando que ela é útil quando uma prova está errada.Menciona a distância entre matemáticos e engenheiros, e espera que também sejam necessárias melhorias de desempenho quando máquinas resolverem matemática.
Expressa decepção com o estado da literatura matemática. Espera que haja problemas na literatura de teoria dos números entre as décadas de 1960 e 1990. Quanto menor a comunidade de especialistas, mais facilmente erros podem passar despercebidos.