Sistemas modernos de inteligência artificial alcançaram a capacidade de resolver problemas matemáticos inéditos e validar demonstrações formais com precisão absoluta. Essa transformação tecnológica acelerou a resolução de conjecturas históricas, mas também abriu uma discussão profunda na comunidade científica sobre o espaço que resta para a intuição, o aprendizado de jovens pesquisadores e a dimensão artística da disciplina.
A base dessa revolução está na chamada prova formal. Tradicionalmente, quando um matemático resolve um problema, ele escreve um artigo em linguagem natural que é lido e avaliado por outros especialistas em um processo de revisão por pares. Esse método manual pode conter pequenos lapsos conceituais. Na abordagem formal, a demonstração é traduzida para linguagens de programação lógicas, como o Lean. Nessas plataformas, o computador atua como um árbitro digital rigoroso, conferindo passo a passo se cada dedução segue exatamente os axiomas, que são as regras fundamentais aceitas sem necessidade de demonstração.
Os modelos de linguagem, que antes apresentavam falhas e imprecisões no raciocínio abstrato, agora utilizam o Lean para testar e corrigir seus próprios passos de maneira autônoma. Se o verificador aponta um erro de lógica, o sistema refaz a linha de raciocínio até encontrar uma cadeia perfeita de deduções comprováveis.
Marcos recentes na matemática pura
A evolução rápida desses sistemas pode ser observada em testes padronizados e em problemas teóricos abertos:
- Desempenho em competições: No teste de referência MiniF2F, composto por problemas no padrão da Olimpíada Internacional de Matemática, a taxa de resolução por sistemas automatizados saltou de cerca de 30% em 2021 para 99,6% com o sistema Seed-Prover, restando apenas um problema não resolvido da lista de álgebra de 2007, conforme documentado em pesquisa sobre modelos de linguagem na fronteira matemática (abre em nova aba).
- O Último Teorema de Fermat: Em setembro de 2026, pesquisadores apresentaram a formalização completa do célebre teorema em um estudo sobre formalização do Último Teorema de Fermat (abre em nova aba). O modelo Claude operou de forma amplamente autônoma durante 11 dias, redigindo 13 milhões de linhas em Lean e provando 29.500 teoremas intermediários apoiado apenas nos axiomas básicos da linguagem.
- Conjecturas clássicas de Erdős: Em maio de 2026, um modelo gerou uma refutação para a conjectura das distâncias unitárias de Erdős. Em agosto de 2026, o relatório de avanços matemáticos da OpenAI (abre em nova aba) detalhou dez resultados obtidos pelo modelo interno Astra, que formulou argumentos posteriormente convertidos por pesquisadores em certificados formais em Lean.
- Exploração em larga escala: Conforme registrado em uma avaliação de busca de provas formais (abre em nova aba), agentes autônomos resolveram 9 de 353 problemas em aberto propostos pelo matemático Paul Erdős, além de provarem 44 conjecturas da Enciclopédia Eletrônica de Sequências de Inteiros a um custo reduzido de processamento computacional.
Comparativo de abordagens matemáticas
| Aspecto | Matemática humana clássica | Prova formal por inteligência artificial |
|---|---|---|
| Validação | Revisão por pares baseada em leitura e consenso | Verificação algorítmica por compiladores como o Lean |
| Método de busca | Intuição, analogia e conexão conceitual profunda | Busca exploratória contínua e autoformalização em larga escala |
| Ritmo de produção | Meses ou anos para elaboração de um manuscrito | Dias ou semanas para geração de milhares de lemas intermediários |
| Linguagem | Textos com linguagem natural e fórmulas | Código de programação rigoroso e estruturado em passos lógicos |
O debate entre intuição artística e automação
A matemática pura sempre foi considerada uma atividade criativa semelhante à poesia e à pintura, caracterizada pela invenção de conceitos totalmente novos, a exemplo dos números imaginários. O avanço da automação levanta a preocupação de que métodos de força bruta computacional privilegiem a quantidade de teoremas concluídos em detrimento da profundidade explicativa.
Em junho de 2026, um grupo de matemáticos publicou uma declaração internacional ressaltando os benefícios da tecnologia, mas alertando para a falta de transparência sobre os métodos das empresas desenvolvedoras e para o risco de antecipar descobertas que costumavam formar pesquisadores iniciantes. Em setembro de 2026, uma declaração intitulada "Um desalinhamento severo da inteligência artificial na matemática" reuniu a assinatura de 25 ganhadores da Medalha Fields. O texto pontua que a produção maciça de demonstrações pode limitar o florescimento de novas ideias conceituais.
Terence Tao, professor da Universidade da Califórnia em Los Angeles e vencedor da Medalha Fields, classificou a formalização como uma faca de dois gumes. Embora reconheça que os sistemas atuais já não podem ser descartados como ferramentas inúteis, Tao criticou a rapidez com que resultados técnicos são despejados no meio acadêmico sem o devido engajamento humano. Segundo ele, as empresas aceleraram a produção justamente porque contam com a verificação formal para atestar o conteúdo.
Helen Wilson, docente da University College London, destacou que a velocidade dos novos agentes pode impedir o trabalho de reflexão gradual dos cientistas. De acordo com a pesquisadora, caso a comunidade acadêmica não acompanhe ou compreenda as demonstrações geradas, o campo corre o risco de se tornar uma indústria de máquinas produzindo artigos que ninguém consegue ler.
Para lidar com essas mudanças, iniciativas de diálogo começaram a ser estruturadas, incluindo a criação de grupos consultivos de matemáticos em laboratórios de inteligência artificial, buscando equilibrar o poder de cálculo dos computadores com a capacidade humana de dar sentido às descobertas.