AI-translated from English; not yet reviewed by a fluent editor.

# Das distâncias unitárias a Navier–Stokes: a matemática com IA entra em uma nova fase

> Da refutação do problema das distâncias unitárias a Navier–Stokes, a matemática com IA avança com novos resultados, desdobramentos humanos e provas formais. O que realmente mudou?

By BIG CHANGE Editorial

Published: 2026-09-22T03:48:27.579Z
Updated: 2026-09-22T03:48:27.579Z
Canonical: https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes

![An open notebook pairs a point-and-line geometry sketch with swirling fluid lines, with an orange pencil beside it.](https://bigchange.ai/api/media/file/geometry-fluid-hero-v1.png)
AI-generated conceptual illustration by BIG CHANGE. From geometry to fluid mathematics: conceptual sketches of the article's range, not the actual unit-distance construction, a proof or a fluid simulation.

Em maio, uma pergunta sobre pontos em um plano produziu uma resposta inesperada. Em setembro, laboratórios de IA publicavam argumentos sobre singularidades de fluidos, junto com arquivos destinados a permitir a verificação das provas por computador. Entre esses anúncios surgiram novos contraexemplos, limites mais fortes e uma formalização do Último Teorema de Fermat.

A mudança na matemática com IA merece mais do que uma contagem contínua de conjecturas derrubadas. Esses resultados respondem a perguntas diferentes, baseiam-se em evidências distintas e deixam trabalhos diferentes por concluir. Um contraexemplo pode derrubar uma hipótese sem encontrar a melhor resposta possível. Um limite aprimorado pode ser importante enquanto a famosa conjectura ao lado continua em aberto. Uma prova verificada por computador pode estabelecer uma afirmação sem explicar por que suas ideias serão úteis em outros contextos.

Esta é nossa análise dos principais avanços entre o anúncio da OpenAI sobre distâncias unitárias, em 20 de maio, e a afirmação de setembro sobre Navier–Stokes, com informações atualizadas até 22 de setembro de 2026. Incluímos anúncios importantes e pesquisas que surgiram nesse intervalo. Este é um mapa dessa sequência, não um inventário completo de todos os artigos de matemática com auxílio de IA. Lemos os anúncios citados, os enunciados relevantes dos teoremas, as introduções das pesquisas e a documentação de verificação. Não atuamos como revisores independentes dessas provas nem reconstruímos suas formalizações.

Nossa avaliação central é que as evidências mais fortes de progresso têm duas partes: máquinas estão produzindo argumentos matemáticos que merecem análise rigorosa, e pessoas já estão extraindo novos resultados matemáticos de alguns desses argumentos. A continuidade do progresso dependerá dos recursos dedicados a verificar, explicar e ampliar esse trabalho.

## Maio: um contraexemplo abre um novo caminho na geometria

O problema das distâncias unitárias é fácil de imaginar. Coloque vários pontos em uma superfície plana e conte os pares que estão exatamente a uma unidade de distância. À medida que você acrescenta pontos, quantos pares podem existir no máximo?

O anúncio da OpenAI, publicado em 20 de maio, atribuiu uma nova construção a um modelo interno de raciocínio de uso geral, avaliado em um conjunto de problemas de Erdős. A empresa também publicou um artigo complementar separado, escrito por matemáticos externos que examinaram o argumento. A existência desse segundo documento importa: os leitores podem verificar o que esses matemáticos compreenderam e reconstruíram, além do relato do laboratório sobre seu modelo. [Anúncio da OpenAI](https://openai.com/index/model-disproves-discrete-geometry-conjecture/).

O manuscrito original constrói infinitos conjuntos de pontos com pelo menos n^(1+δ) pares a distância unitária, para um δ positivo fixo. Em termos simples, a melhora no expoente persiste à medida que os exemplos crescem. Isso contradiz a conjectura de crescimento quase linear. Não determina o número máximo exato de distâncias unitárias para cada quantidade de pontos, e a busca mais ampla por limites ótimos continua. [Manuscrito sobre distâncias unitárias](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf).

A surpresa estava na origem da construção. O artigo complementar relaciona o resultado geométrico à teoria algébrica dos números avançada e cita contribuições matemáticas anteriores. Seus autores apresentam uma reconstrução simplificada e um tanto generalizada. Este é um exemplo útil do trabalho humano após uma descoberta por IA: identificar o mecanismo, tornar visíveis suas dependências e transformar um argumento em algo que outros pesquisadores possam explorar. [Artigo complementar dos matemáticos](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-remarks.pdf).

Assim, quem procura entender a importância do resultado de maio deve acompanhar os artigos subsequentes tão de perto quanto o anúncio inicial. Uma nova técnica ganha outro tipo de credibilidade quando pesquisadores a utilizam para formular e responder perguntas adicionais.

## De maio a julho: as ideias começam a circular

Em 27 de maio, Thomas Bloom, Will Sawin, Carl Schildkraut e Dmitrii Zhelezov publicaram um contraexemplo à conjectura soma-produto nos números reais. Em linhas gerais, o problema diz respeito ao quanto um conjunto se expande quando seus elementos são somados ou multiplicados entre si. A construção permite que ambos os conjuntos resultantes permaneçam menores do que a escala quase quadrática conjecturada. Os autores afirmam explicitamente que o contraexemplo das distâncias unitárias os levou a reconsiderar corpos numéricos de grau elevado. Também explicam que a construção final exige menos teoria dos números do que o resultado anterior. [Artigo sobre soma-produto](https://arxiv.org/html/2605.28781v1).

Este é um exemplo concreto de um resultado originado por IA que estimulou a matemática produzida por seres humanos. Isso não demonstra que uma IA escreveu o artigo subsequente, e não devemos apagar os nomes de seus autores incorporando o trabalho à contagem de sucessos de um laboratório.

O preprint de Cosmin Pohoata, enviado pela primeira vez em 11 de junho e revisado em 28 de junho, dá continuidade à sequência no problema de Elekes–Rónyai. Ele apresenta um exemplo polinomial cujos valores em conjuntos adequados se expandem menos do que o esperado, usando elementos das construções recentes sobre distâncias unitárias e soma-produto. O artigo explicita a relação entre os problemas. [Artigo de Pohoata](https://arxiv.org/html/2606.13619v2).

Em 6 de julho, Sungchul Lee, Pohoata e Daniel Zhu publicaram outro resultado sobre a grade de Minkowski. Sua construção preserva propriedades de distâncias repetidas dentro de subconjuntos, com consequências para questões que envolvem distâncias repetidas e triângulos isósceles. Isso revela uma estrutura mais rica do que apenas apresentar uma configuração excepcional e deixar sem análise seu comportamento interno. [Artigo sobre a grade de Minkowski](https://arxiv.org/html/2607.05374v1).

Há evidências favoráveis a uma interpretação otimista. O resultado de maio forneceu material que outros pesquisadores conseguiram modificar e reutilizar em poucas semanas. Propomos medir o sucesso pela produção de métodos utilizáveis, junto com o esforço necessário para compreendê-los. Uma simples contagem de problemas resolvidos não mostraria essa distinção.

## Julho: o contraexemplo do jacobiano mostra por que o escopo importa

Um segundo episódio notável envolveu a conjectura jacobiana. A exposição de Terence Tao, publicada em 21 de julho, examina um contraexemplo produzido com o Fable AI: uma aplicação polinomial em três variáveis complexas que se comporta como invertível em uma pequena vizinhança, mas envia pontos distintos à mesma imagem quando considerada no todo. A afirmação geral da conjectura falha em três dimensões ou mais; o caso bidimensional continua em aberto. Tao apresenta fórmulas explícitas e explica a geometria da construção. [Exposição matemática de Tao](https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the-jacobian-conjecture-counterexample/).

Um contraexemplo explícito pode tornar sua contradição essencial relativamente acessível a cálculos. Descobrir por que tal exemplo deveria existir e como construir outros semelhantes exige mais trabalho matemático. O episódio da conjectura jacobiana permite aos leitores observar essas diferentes tarefas em publicações.

A distinção continuou importante em setembro. O preprint de 15 de setembro de Arno van den Essen apresenta um caminho elementar para um contraexemplo equivalente, após mudanças lineares de coordenadas, ao exemplo encontrado por Levent Alpöge. Trata-se de uma nova explicação da construção, não de uma segunda refutação independente da conjectura original. [Artigo de van den Essen](https://arxiv.org/abs/2609.17795).

Para um gestor de pesquisa, isso sugere uma mudança prática no que deve ser recompensado. Financiar a pessoa que torna compreensível uma descoberta complexa pode liberar tanto trabalho subsequente quanto financiar outra busca por um resultado de destaque. Essa é nossa avaliação da sequência, não uma afirmação de que as universidades já mudaram seus incentivos.

## Agosto: uma variedade maior de afirmações matemáticas

O lançamento da OpenAI em 1º de agosto apresentou dez grupos de resultados em matemática e ciência da computação teórica. Segundo a empresa, uma versão interna do Astra gerou os argumentos; humanos trabalharam com o modelo para preparar os manuscritos, e o modelo produziu certificados do Lean. Esse relato da produção difere do anúncio de um único resultado em maio e explicita a contribuição da preparação dos manuscritos. [Anúncio de agosto](https://openai.com/index/ten-advances-in-mathematics/).

A coletânea que acompanhou o anúncio, atualizada em 6 de agosto, apresenta os resultados a seguir. São descrições das afirmações dos manuscritos, não dez certificações independentes feitas pela BIG CHANGE:

- **Empacotamento de esferas:** um limite superior assintótico mais preciso em dimensões elevadas.
- **Códigos binários e esféricos:** limites mais fortes para os tamanhos de códigos com separações especificadas.
- **Teoria de grupos:** construção de um grupo não-sofico.
- **Álgebras de operadores:** contraexemplos à conjectura de rigidez de Connes.
- **Complexidade aritmética:** limites inferiores mais fortes para circuitos e fórmulas do permanente.
- **Jogos quânticos:** um teorema de repetição paralela exponencial.
- **Problemas de reticulados:** resultados mais fortes de dureza de aproximação para o problema do vetor mais próximo.
- **Geometria convexa:** uma prova da conjectura de volume de Ehrhart.
- **Teoria de Ramsey:** um limite inferior superexponencial para números de Ramsey de triângulos com várias cores.
- **Teoria extremal dos grafos:** contraexemplos às conjecturas de compacidade e degenerescência.

[Coletânea de pesquisas sobre os dez resultados](https://cdn.openai.com/pdf/ten-proofs-oai.pdf).

A variedade é importante, mas também torna enganosa uma única pontuação total. Encontrar um contraexemplo, melhorar um limite e provar um teorema geral têm consequências diferentes. E um resultado sobre a dificuldade de um problema matemático não demonstra automaticamente um ataque a um sistema criptográfico em uso. As aplicações exigem uma cadeia própria de raciocínio e evidências.

Em 10 de agosto, a Anthropic publicou um avanço de escopo mais restrito relacionado à hipótese de Riemann. A empresa afirma que um modelo Claude ainda não lançado melhorou o limite inferior para a proporção de zeros zeta na linha crítica. Matemáticos da Anthropic examinaram o trabalho, especialistas externos revisaram o artigo e foi produzida uma formalização. A empresa declara expressamente que Claude não resolveu a hipótese de Riemann e que não espera que essas técnicas o façam. [Relato da Anthropic](https://www.anthropic.com/research/riemann-zeta).

O artigo vinculado apresenta um limite um pouco acima de dois terços, aproximadamente 67,25%, e identifica os resultados analíticos anteriores de que depende. Trata-se de uma afirmação matemática assintótica, não da alegação de que a análise de uma grande amostra finita de zeros prova a hipótese. A distinção é essencial: um limite inferior para a proporção não coloca todos os zeros relevantes sobre a linha. [Manuscrito sobre os zeros zeta](https://www-cdn.anthropic.com/95c246936988e43127bc6b2ceb7077c1dad2d68e.pdf).

Também circulam outros manuscritos ambiciosos. Um documento hospedado no site de Alpöge propõe uma estrutura complexa na esfera de dimensão seis. A construção está disponível para exame, mas a cópia que consultamos não permite estabelecer uma data confiável para o anúncio nem um relato completo da contribuição da IA. Por isso, incluímos o trabalho como uma proposta que os leitores podem investigar, sem elevá-lo a um marco estabelecido de forma independente nesta cronologia. [Manuscrito sobre a esfera de dimensão seis](https://alpo.ge/s6.pdf).

## Início de setembro: lacunas entre primos revelam um limite de verificação

A sequência de anúncios também chegou às lacunas entre números primos. Um artigo preliminar, publicado em 3 de setembro pela colaboração Axiom, afirma que infinitos pares de primos consecutivos estão separados por no máximo 212. Ele reconhece o trabalho analítico de Julia Stadlmann e o projeto Polymath anterior. Seu certificado do Lean também pressupõe estimativas analíticas e um certificado variacional verificado separadamente. Isso faz avançar a questão dos intervalos limitados entre primos; a conjectura dos primos gêmeos exige infinitas lacunas exatamente iguais a dois. [Artigo da equipe Axiom](https://primegaps.axiommath.ai/bgp212.pdf).

O repositório público PrimeGaps186 da OpenAI apresenta um limite ainda menor, com uma ressalva crucial. Seu desenvolvimento no Lean depende de três axiomas de entrada que não foram provados, cobrindo duas estimativas da literatura e limites numéricos de integrais. O repositório declara que o certificado numérico não prova esses axiomas. Portanto, os leitores devem distinguir o argumento matemático proposto da parte formalmente verificada sob entradas especificadas. Seria incorreto descrever esse artefato como uma prova incondicional, totalmente formal, baseada apenas nos axiomas fundamentais. [Repositório PrimeGaps186](https://github.com/openai/PrimeGaps186).

Outro manuscrito da OpenAI trata de lacunas longas: o tamanho que podem alcançar os intervalos entre primos consecutivos. Ele apresenta um limite inferior aprimorado para as maiores lacunas abaixo de um limiar crescente. Essa questão extremal é diferente de encontrar infinitos pares de primos próximos; o progresso em uma não deve ser contado como solução da outra. [Manuscrito sobre lacunas longas](https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/long_gaps.pdf).

Esses detalhes tornam o episódio das lacunas entre primos particularmente útil. Dois números em uma manchete podem parecer parte de uma corrida simples. Quando as dependências da prova ficam visíveis, a pergunta mais relevante é quais etapas foram estabelecidas por quais métodos. Explicitar as hipóteses é valioso mesmo quando a formalização continua incompleta.

## 4 de setembro: a formalização passa a integrar a história da descoberta

O anúncio da Anthropic, publicado em 4 de setembro, diz respeito a um teorema cuja prova matemática já era conhecida: o Último Teorema de Fermat. A conquista alegada é uma formalização completa no Lean, produzida em grande parte de forma autônoma por Claude ao longo de onze dias. A empresa descreve a orientação humana e uma plataforma de colaboração que ajudou os agentes a acompanhar as dependências. Ela reconhece a tradição de provas matemáticas em que o trabalho se baseia. [Anúncio da formalização](https://www.anthropic.com/research/formalizing-fermats-last-theorem).

O repositório público fornece evidências mais específicas do que a manchete. Ele enuncia o teorema, registra dependências e documenta verificações em relação aos axiomas padrão do Lean e à formulação do enunciado no Mathlib. Também se descreve como um artefato de pesquisa sem manutenção. Examinamos essa documentação; não executamos novamente a compilação. [Repositório do Último Teorema de Fermat](https://github.com/anthropics/fermats-last-theorem).

Se as mesmas ferramentas que produzem mais argumentos candidatos também ajudam a formalizá-los, a capacidade de verificação pode crescer. Isso é um motivo substancial para otimismo. Pesquisadores futuros ganham algo concreto para inspecionar. Ainda precisam saber se os resultados intermediários são fáceis de reutilizar, se as dependências continuam compiláveis e quem mantém o artefato. O volume de código gerado, por si só, não responde a essas perguntas.

Aqui há uma escolha institucional importante. Um laboratório pode divulgar uma prova como demonstração concluída de seu modelo ou mantê-la como infraestrutura para o trabalho de outras pessoas. Essas abordagens criam obrigações diferentes após o lançamento. Manutenção, exemplos explicativos e referências estáveis devem fazer parte do orçamento de pesquisa.

## 8 de setembro: o que o resultado de Navier–Stokes realmente afirma

O resultado sobre fluidos deixa essas questões ainda mais claras. O anúncio da OpenAI, publicado em 8 de setembro e atualizado em 10 de setembro, apresenta uma solução proposta para o problema de existência e suavidade de Navier–Stokes. A empresa atribui o trabalho a um modelo interno que opera por meio de agentes coordenadores e divulga um argumento escrito e uma formalização no Lean. A OpenAI diz que não pretende pleitear o Prêmio Millennium. [Anúncio da OpenAI](https://openai.com/index/navier-stokes-solution/).

O manuscrito trata do movimento de um fluido incompressível tridimensional com viscosidade positiva e uma força externa construída cuidadosamente. Partindo do repouso, a solução proposta desenvolve velocidade ilimitada em tempo finito, embora sua energia total permaneça limitada. A força é suave e confinada no espaço e no tempo. Sua construção matemática usa um vórtice em colapso e correções organizadas para que a força resultante permaneça suave. São afirmações sobre soluções de equações, não observações de um experimento físico nem um novo simulador de engenharia. [Manuscrito de Navier–Stokes](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf).

A força externa é fundamental para entender o escopo. A descrição oficial do problema do Clay apresentada por Charles Fefferman permite forças suaves nas alternativas de quebra C e D. As alternativas A e B, de suavidade global, tratam das equações sem força externa. Portanto, um resultado válido do tipo proposto pode responder a uma alternativa explicitamente permitida pelo Clay e deixar sem solução a questão da regularidade global sem força externa. Dizer que a força é irrelevante exageraria o teorema; descartar o resultado por estar fora do problema declarado descreveria incorretamente as regras. [Enunciado oficial do problema](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf).

A OpenAI também divulgou um argumento separado sobre Euler, que trata de um fluido idealizado sem viscosidade. Esse manuscrito propõe uma quebra em tempo finito a partir de dados iniciais suaves, sem força externa. Euler e Navier–Stokes são equações relacionadas, mas as hipóteses e conclusões desses dois artigos devem ser mantidas separadas. [Manuscrito sobre Euler](https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf).

O histórico de pesquisas em torno do resultado também importa. Em sua declaração de 10 de setembro, a Sociedade Europeia de Matemática reconhece as contribuições de Córdoba, Martínez-Zoroa e Zheng, além das de Alpöge, Buckmaster e de matemáticos anteriores. A declaração também levanta questões de acesso, autoria e reconhecimento. Um relato que salta diretamente do nome de um modelo para um teorema deixa de lado o acúmulo de ideias que tornou o trabalho possível. [Declaração da EMS](https://euromathsoc.org/news/ems-statement-on-recent-navier-stokes-announcement-225).

Em 11 de setembro, o Clay respondeu com entusiasmo cauteloso sobre a aparente resolução e afirmou que a avaliação e a atribuição de créditos seguiriam um processo deliberadamente sem pressa. É uma resposta institucional relevante. Não é um anúncio de premiação nem uma declaração de que todos os aspectos do trabalho concluíram a revisão. [Anúncio do Clay](https://www.claymath.org/news/navier-stokes-announcement/).

Para os leitores, a conclusão precisa já é suficientemente significativa, sem acréscimos: um laboratório de IA divulgou uma prova proposta para um problema reconhecido do Prêmio Millennium, acompanhada de artefatos matemáticos e formais que podem ser inspecionados, e grandes instituições estão levando o trabalho a sério. A aceitação mais ampla, a atribuição de créditos e a compreensão ainda dependem de processos com etapas por cumprir.

![Manuscript pages lead to a magnifying glass over a statement and dependency pages, then to an explanatory book and reusable pages.](/api/media/file/proposal-check-understanding-inline-v2.png)

## A verificação de uma prova responde a uma pergunta precisa

A verificação formal muda as evidências disponíveis aos revisores. Também deve tornar a cobertura mais precisa.

A própria documentação do Lean distingue a validade de uma prova do significado do enunciado provado. Uma verificação básica bem-sucedida estabelece que um enunciado formal decorre de suas definições e hipóteses. Verificações adicionais podem revelar dependências incompletas, auditar axiomas e comparar a prova com um enunciado especificado de forma independente. A documentação descreve verificações mais robustas por meio de verificadores externos e ainda identifica hipóteses remanescentes. [Guia de validação do Lean](https://lean-lang.org/doc/reference/latest/ValidatingProofs/).

Imagine um pesquisador que precise de um limite válido para todas as entradas de um algoritmo. Um assistente fornece um teorema formalmente correto, mas a definição de entrada admissível exclui uma categoria difícil. A prova pode estar correta sem dar suporte à aplicação do pesquisador. É um exemplo hipotético de por que a tradução da pergunta para o enunciado formal precisa de atenção.

A novidade exige outro tipo de verificação. Um sistema de provas não determina se o mesmo argumento apareceu com outra terminologia em um artigo antigo, se o reconhecimento das contribuições está completo ou se a melhora alegada faz alguma diferença importante para a aplicação. Essas avaliações exigem pesquisa bibliográfica e conhecimento especializado.

Por isso, pediríamos a um laboratório que divulga um resultado importante que forneça um pacote duradouro: a afirmação exata em linguagem matemática comum, sua formulação formal quando disponível, a prova e suas dependências, um relato claro das contribuições humanas e do modelo e o registro do que foi revisado e alterado. Esse é o padrão de divulgação que propomos. Ele permite que outros pesquisadores identifiquem as responsabilidades e reproduzam as verificações relevantes.

## O grupo consultivo aborda um problema crescente de coordenação

O anúncio de 21 de setembro do Grupo Consultivo sobre Matemática e Inteligência Artificial surge nesse contexto. O grupo afirma ser independente, não remunerado e disposto a aconselhar qualquer empresa de IA pertinente. Sua tarefa imediata é assessorar a OpenAI sobre a divulgação de novos resultados que, segundo a empresa, obteve. O grupo promete recomendações públicas e afirma expressamente que não tem poder decisório nas empresas. A declaração publicada no blog de Terence Tao é uma postagem de convidado do grupo. [Declaração do grupo](https://agmai.org/).

A OpenAI descreve um mandato que envolve revisão, comunicação, relevância e divulgação. Também diz que o grupo não é responsável por aconselhar sobre o ritmo do progresso matemático interno. Portanto, o papel consultivo deve ser entendido como um canal de análise e coordenação, com as decisões permanecendo na empresa. [Anúncio da OpenAI sobre o grupo consultivo](https://openai.com/index/advisory-group-on-mathematics-and-ai/).

Há motivos para acolher esse arranjo. Uma coordenação melhor pode reduzir trabalho de revisão duplicado, identificar os especialistas adequados e garantir que a descrição de um resultado corresponda às evidências que o sustentam. Seus limites também são claros: é preciso responder às recomendações, e a independência, por si só, não cria um mecanismo de aplicação. Os leitores devem acompanhar as recomendações publicadas e o que as empresas farão com elas.

A perspectiva cética também diz respeito à finalidade da pesquisa. A declaração Matemática e IA, de 11 de setembro, argumenta que uma corrida para resolver problemas listados pode negligenciar o desenvolvimento da compreensão e a formação de futuros matemáticos. Os signatários descrevem um risco para os processos pelos quais as ideias se tornam ensináveis e úteis. É uma posição séria de participantes da disciplina, não uma medição que demonstre que todo uso de IA já a prejudicou. [A declaração](https://mathandai.org/).

Henry Cohn desenvolve um argumento relacionado em um ensaio publicado como convidado no blog de Tao em 15 de setembro: resultados mal explicados podem impor muito trabalho à comunidade que precisa assimilá-los. Sua preocupação também abrange os incentivos para quem realiza esse trabalho explicativo. A atribuição correta importa aqui: o ensaio é de Cohn, embora esteja hospedado por Tao. [Ensaio de Cohn](https://terrytao.wordpress.com/2026/09/15/the-technical-debt-of-ai-generated-mathematics/).

## O próximo avanço deve ser mais fácil para outra pessoa utilizar

A sequência de maio a setembro sustenta uma interpretação esperançosa, com exemplos concretos. Um contraexemplo geométrico inspirou novas construções. Pesquisadores encontraram maneiras mais claras de explicar uma aplicação polinomial surpreendente. A formalização produziu artefatos adicionais que permitem inspecionar raciocínios complexos. Estão visíveis os ingredientes para uma relação produtiva entre os resultados de modelos e a prática matemática.

O cenário pessimista também é concreto. Laboratórios poderiam gerar resultados propostos mais depressa do que outras pessoas conseguem compreendê-los e, depois, contabilizar os anúncios como contribuições científicas concluídas. A revisão poderia se tornar um fardo imposto a um pequeno grupo de especialistas, enquanto recursos e prestígio fluiriam para os sistemas que produzem esse acúmulo. O acesso limitado aos modelos poderia aprofundar o desequilíbrio entre quem gera descobertas e quem deve avaliá-las.

Na nossa avaliação, laboratórios, financiadores e periódicos deveriam medir os dois lados do processo. Contabilizar descobertas candidatas, mas também a análise independente, as simplificações úteis, os argumentos corrigidos, as bibliotecas formais reutilizáveis e os trabalhos subsequentes. Reconhecer as pessoas que tornam um resultado inteligível. Publicar correções com a mesma persistência que os anúncios.

Para um leitor que acompanha o próximo avanço, a pergunta mais reveladora é específica: o que outro pesquisador pode fazer agora que não podia fazer antes? A resposta pode ser construir um contraexemplo, estabelecer uma garantia mais forte, verificar um argumento difícil ou ensinar um método novo. É assim que o avanço da matemática com IA se transforma em avanço da matemática.

## Sources

- [OpenAI: anúncio sobre distâncias unitárias](https://openai.com/index/model-disproves-discrete-geometry-conjecture/) — 20 de maio de 2026. Confirma a data de divulgação e o relato da empresa sobre a participação do modelo e a revisão externa. As afirmações de prioridade e autonomia não são uma avaliação independente de todas as etapas da produção.
- [OpenAI: conjuntos de pontos planares com muitas distâncias unitárias](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf) — Divulgado junto com o anúncio de 20 de maio. O resumo e o teorema principal apresentam uma família infinita com melhora fixa e positiva no expoente. O contraexemplo não determina a função extremal exata; não atuamos como revisores da prova.
- [Alon e colegas: observações sobre a refutação do problema das distâncias unitárias](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-remarks.pdf) — Artigo complementar da divulgação de maio. Apresenta uma reconstrução verificada por matemáticos, algumas simplificações e generalizações e o reconhecimento de contribuições anteriores em teoria dos números. Ler as afirmações não equivale a verificar independentemente cada etapa matemática.
- [Bloom, Sawin, Schildkraut e Zhelezov: a conjectura soma-produto é falsa nos números reais](https://arxiv.org/html/2605.28781v1) — Preprint de 27 de maio. A introdução reconhece explicitamente que o contraexemplo das distâncias unitárias foi uma inspiração. Trata-se de pesquisa subsequente escrita por humanos; sua inclusão não atribui a prova à OpenAI nem demonstra aceitação por um periódico.
- [Cosmin Pohoata: primos partidos e o problema de Elekes–Rónyai](https://arxiv.org/html/2606.13619v2) — Enviado pela primeira vez em 11 de junho e revisado em 28 de junho. Apresenta um contraexemplo de expansão polinomial e explica o uso de construções recentes. As datas são das versões do preprint, não de um suposto primeiro anúncio público.
- [Lee, Pohoata e Zhu: a grade de Minkowski tem muitas distâncias repetidas de forma robusta](https://arxiv.org/html/2607.05374v1) — Preprint de 6 de julho. Estabelece as afirmações dos autores sobre a robustez das distâncias repetidas em subconjuntos e suas consequências. Resumimos seu escopo e a inspiração documentada, sem provar as estimativas de forma independente nem sugerir autoria de IA.
- [Terence Tao: uma análise do contraexemplo à conjectura jacobiana](https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the-jacobian-conjecture-counterexample/) — Exposição matemática de Tao publicada em 21 de julho, com uma aplicação explícita e explicação. Distingue o contraexemplo em três dimensões ou mais do caso bidimensional em aberto. Não utilizamos afirmações não verificadas dos comentários.
- [Arno van den Essen: uma maneira elementar de encontrar um contraexemplo à conjectura jacobiana](https://arxiv.org/abs/2609.17795) — Preprint de 15 de setembro. Sua contribuição declarada é um caminho elementar para um exemplo equivalente ao de Alpöge sob mudanças de coordenadas. Trata-se de trabalho explicativo subsequente, não de evidência de uma segunda descoberta independente de contraexemplo.
- [OpenAI: dez avanços em matemática e ciência da computação teórica](https://openai.com/index/ten-advances-in-mathematics/) — Anúncio de 1º de agosto. Descreve a divisão de trabalho alegada entre o modelo interno, os humanos que prepararam os manuscritos e a formalização pelo modelo. Omitimos a comparação de custos em tokens da empresa e não tratamos o lançamento como revisão independente.
- [OpenAI: coletânea de pesquisas sobre os Dez Avanços](https://cdn.openai.com/pdf/ten-proofs-oai.pdf) — Coletânea atualizada em 6 de agosto, após o lançamento de 1º de agosto. A lista resumida do artigo apresenta as dez áreas relatadas. Lemos o resumo, o sumário e enunciados selecionados de teoremas, não as 253 páginas na condição de revisores.
- [Anthropic: conheça melhor as capacidades matemáticas do Claude](https://www.anthropic.com/research/riemann-zeta) — Anúncio de 10 de agosto, atualizado em 13 de agosto. Descreve a pesquisa sobre zeros zeta e as verificações humanas e afirma expressamente que a hipótese de Riemann continua sem solução. Os relatos sobre o processo do modelo e a validação são atribuídos à Anthropic.
- [Claude/Anthropic: zeros da função zeta de Riemann](https://www-cdn.anthropic.com/95c246936988e43127bc6b2ceb7077c1dad2d68e.pdf) — Manuscrito datado de 11 de agosto, vinculado ao anúncio atualizado em 13 de agosto. O resumo e o Teorema A distinguem proporções assintóticas, simplicidade e posição na linha crítica. A constante refinada é aproximadamente 0,6725; não há prova da hipótese completa.
- [Manuscrito de Alpöge sobre a esfera de dimensão seis](https://alpo.ge/s6.pdf) — Cópia sem data, consultada em 22 de setembro. O título e a introdução descrevem uma estrutura complexa proposta para a esfera de dimensão seis. Não foi possível estabelecer, com esse material, uma data confiável de divulgação nem a contribuição completa da IA; por isso, permanece uma proposta qualificada.
- [Charton e colegas: um novo limite para pequenas lacunas entre primos](https://primegaps.axiommath.ai/bgp212.pdf) — Rascunho preliminar de 3 de setembro. O resumo e o Teorema 1.1 apresentam o limite 212 e reconhecem trabalhos anteriores. O certificado Lean do Apêndice A pressupõe entradas analíticas e um certificado variacional verificado separadamente; a prova não está totalmente formalizada a partir de axiomas fundamentais.
- [OpenAI: repositório PrimeGaps186](https://github.com/openai/PrimeGaps186) — Repositório atual consultado em 22 de setembro. O README identifica explicitamente três axiomas de entrada não provados no desenvolvimento do Lean. O certificado numérico não os demonstra. Consultamos a documentação sem executar a compilação ou o certificado numérico.
- [OpenAI: grandes lacunas entre primos consecutivos](https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/long_gaps.pdf) — Manuscrito vinculado ao lançamento do Astra de 3 de setembro. Seu teorema trata de um limite inferior para a maior lacuna entre primos abaixo de um limiar crescente. É diferente de afirmações sobre pequenas lacunas ou primos gêmeos; não verificamos a prova de forma independente.
- [Anthropic: formalização do Último Teorema de Fermat](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — Anúncio de 4 de setembro. Relata um esforço de formalização de onze dias e descreve a coordenação e a orientação humana. Trata-se da verificação de uma matemática conhecida; os relatos sobre o cronograma e a autonomia são da própria empresa.
- [Anthropic: repositório do Último Teorema de Fermat](https://github.com/anthropics/fermats-last-theorem) — Repositório atual consultado em 22 de setembro. Documenta o enunciado, as dependências, as verificações de axiomas e a comparação com o Mathlib. Classifica o lançamento como um artefato de pesquisa sem manutenção. Não executamos novamente nem validamos independentemente a prova formal.
- [OpenAI: sobre o Problema do Prêmio Millennium de Navier–Stokes](https://openai.com/index/navier-stokes-solution/) — Anúncio de 8 de setembro, atualizado em 10 de setembro. Confirma a afirmação do laboratório, o relato de produção com agentes e a decisão de não pleitear o prêmio. Não decidimos disputas privadas sobre procedência nem equiparamos o anúncio à conclusão da análise pela comunidade.
- [OpenAI: manuscrito sobre Navier–Stokes](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf) — Divulgado em 8 de setembro. A introdução e o Teorema 1.1 descrevem viscosidade positiva, força suave de suporte compacto, repouso inicial, energia limitada e explosão da velocidade em tempo finito. Esse é o escopo do teorema proposto, não uma verificação independente nossa.
- [Charles Fefferman: descrição oficial do problema de Navier–Stokes](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf) — Formulação oficial do Clay, consultada em 22 de setembro. As alternativas C e D permitem forças suaves; A e B formulam questões de suavidade sem força externa. Não usamos o diretório de envio incluído no URL como data original de publicação.
- [OpenAI: manuscrito sobre Euler](https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf) — Divulgado junto com o material de 8 de setembro. O Teorema 1.1 trata de dados suaves e sem força externa para Euler e de quebra em tempo finito das derivadas ou da vorticidade. Suas equações e conclusões não devem ser confundidas com a afirmação separada sobre Navier–Stokes com força externa.
- [Sociedade Europeia de Matemática: declaração sobre o anúncio de Navier–Stokes](https://euromathsoc.org/news/ems-statement-on-recent-navier-stokes-announcement-225) — Declaração de 10 de setembro. Reconhece contribuições matemáticas contemporâneas e anteriores e discute acesso e reconhecimento. Oferece contexto institucional; não é um certificado de prova independente nem uma resolução de todas as questões de prioridade.
- [Instituto Clay de Matemática: anúncio sobre Navier–Stokes](https://www.claymath.org/news/navier-stokes-announcement/) — Resposta de 11 de setembro que emprega linguagem cautelosa sobre a aparente resolução e descreve um processo deliberado de avaliação. Demonstra atenção institucional séria, não que o Prêmio Millennium tenha sido concedido.
- [Lean: validação de uma prova no Lean](https://lean-lang.org/doc/reference/latest/ValidatingProofs/) — Documentação oficial atual, consultada em 22 de setembro. Distingue validade da prova, significado do enunciado, auditorias de axiomas e métodos de verificação mais robustos. A verificação formal oferece garantias específicas sob certas hipóteses; não estabelece novidade, crédito ou utilidade.
- [Grupo Consultivo sobre Matemática e Inteligência Artificial](https://agmai.org/) — Grupo lançado em 21 de setembro, com a mesma declaração publicada como postagem de convidado no blog de Tao. Confirma sua independência sem remuneração, o compromisso com recomendações públicas e a falta de poder decisório nas empresas. A nova leva de resultados continua atribuída à OpenAI.
- [OpenAI: Grupo Consultivo sobre Matemática e IA](https://openai.com/index/advisory-group-on-mathematics-and-ai/) — Anúncio de 21 de setembro. Descreve o mandato consultivo e exclui expressamente aconselhar sobre o ritmo do progresso matemático interno. Omitimos o total alegado de novos resultados porque sua correção e novidade agregadas não foram estabelecidas de forma independente nesta análise.
- [Matemática e IA: um grave desalinhamento da IA na matemática](https://mathandai.org/) — Declaração de 11 de setembro. Apresenta o argumento de matemáticos sobre compreensão, ensino, atribuição de créditos e incentivos. É uma manifestação de participantes da disciplina, não uma medição controlada dos efeitos de todo uso de IA.
- [Henry Cohn: o débito técnico da matemática gerada por IA](https://terrytao.wordpress.com/2026/09/15/the-technical-debt-of-ai-generated-mathematics/) — Ensaio de Henry Cohn publicado como convidado no blog de Tao em 15 de setembro. Discute explicações e o trabalho necessário para assimilar resultados. Atribuímos o argumento a Cohn e o distinguimos de uma estimativa empírica do custo da revisão.