Prova da Conjectura de Poincaré é formalizada com auxílio de IA
Equipe de matemáticos utilizou o assistente Lean e ferramentas de IA para validar formalmente a prova da Conjectura de Poincaré em 3D.
Pontos principais
- A formalização completa da prova de Hamilton-Perelman foi publicada no repositório arXiv em setembro de 2026.
- O projeto utilizou o assistente de prova Lean 4 para verificar rigorosamente cada passo do argumento matemático.
- O código final totaliza cerca de 4,7 milhões de linhas, sendo 2,7 milhões geradas nas duas semanas finais com auxílio de IA.
- A equipe foi liderada pelo professor Bennett Chow, da Universidade da Califórnia em San Diego (UCSD).
- A prova formal não contém lacunas, passando integralmente pela verificação do kernel do sistema Lean.
- O trabalho abrange tanto a versão suave da conjectura quanto o teorema de suavização de Moise.
Uma equipe de pesquisadores liderada pelo matemático Bennett Chow concluiu a formalização completa da prova da Conjectura de Poincaré tridimensional, um dos sete Problemas do Milênio. O trabalho, que valida o método de fluxo de Ricci desenvolvido por Richard Hamilton e Grigori Perelman, foi registrado no sistema de verificação Lean 4 e publicado no arXiv. A conquista marca um avanço significativo na matemática computacional, ao demonstrar a viabilidade de utilizar assistentes de prova para verificar teoremas de alta complexidade.
O projeto exigiu a escrita de aproximadamente 4,7 milhões de linhas de código, das quais cerca de 2,7 milhões foram produzidas em um esforço intensivo de duas semanas com o suporte de modelos de linguagem como ChatGPT e Claude. A equipe, composta também por Ziyang Qin, Yuan Liao e Ayush Khaitan, garantiu que todo o conjunto de dados passasse pela verificação rigorosa do kernel do Lean, sem o uso de marcadores de pendência. Esta formalização estabelece um novo patamar para a verificação automatizada de provas matemáticas de grande escala.
Comentários
Carregando comentários...