IA derruba conjectura de 1946: matemática mudou

O contraexemplo que ninguém esperava

IA boa em matemática não é novidade quando o assunto é prova de vestibular ou olimpíada. O jogo mudou quando um modelo interno da OpenAI encontrou um contraexemplo para a conjectura da distância unitária de Erdős, aberta desde 1946. Não foi uma solução elegante encontrada por intuição humana, foi uma refutação direta a um problema que sobreviveu a gerações de especialistas. Um mês depois veio a prova do Cycle Double Cover, depois mais dez problemas abertos até julho e um resultado ligado a Navier Stokes em setembro. A Anthropic respondeu com formalização do último teorema de Fermat e avanços em limites ligados à hipótese de Riemann. Isso não é mais benchmark escolar, é pesquisa original.

O fato é seco e por isso assusta. Modelos que até ontem alucinavam em aritmética básica agora operam no nível onde humanos passam anos travados. Para quem constrói com LLM, a pergunta não é se isso é impressionante, é se dá para prever onde essa capacidade funciona. Nem todo problema aberto é igual para uma máquina. Alguns caem rápido, outros continuam impossíveis. Entender essa diferença decide onde vale a pena apontar GPU e tempo de engenharia.

O fato: de Erdős a Navier-Stokes

A conjectura de Erdős perguntava algo simples de enunciar e brutal de provar, sobre quantas vezes a distância unitária pode se repetir em um conjunto grande de pontos no plano. Muita gente tentou provar que o limite era baixo. A IA fez o contrário, mostrou que o limite estoura ao construir um conjunto que viola a conjectura. O comentário mais rico veio do matemático Timothy Gowers, que reconstruiu a lógica da prova e tentou medir sua dificuldade real. Depois disso o ritmo acelerou, com CDC, que trata de cobrir todo grafo sem pontes com ciclos, e outros resultados encadeados em poucas semanas.

O ponto importante é que não foi sorte isolada. Foram vários resultados em sequência, com técnicas diferentes, envolvendo construção explícita, prova assistida e formalização. Formalizar Fermat, por exemplo, não é descobrir matemática nova, é traduzir uma prova humana gigantesca para uma linguagem que a máquina consegue verificar sem ambiguidade. Já o contraexemplo de Erdős e o CDC envolvem criatividade combinatorial, busca em espaços enormes e generalização de construções conhecidas. São modos diferentes de usar o modelo, e isso importa para quem quer replicar.

Como funciona: hints, trabalho e complexidade

A melhor explicação até agora usa um modelo mental simples. Resolver um problema difícil é encadear insights com muito trabalho entre eles. Você tem uma ideia, passa meses desenvolvendo, trava, tem outra ideia, avança mais um pouco. Gowers chama isso de complexidade de Kolmogorov módulo especialistas, que é basicamente o tamanho da menor sequência de dicas que permitiria a um expert reconstruir a prova. No caso da distância unitária, foram três dicas centrais. Primeiro, procure um contraexemplo em vez de tentar provar. Segundo, pegue a melhor construção conhecida e generalize. Terceiro, teste uma sequência de corpos de números de grau crescente, mas trabalhe com ideais primos de norma limitada.

Parece simples depois de lido, e esse é o ponto. Uma boa dica parece óbvia depois e improvável antes. Quase ninguém apostava de verdade no contraexemplo. A fórmula proposta para dificuldade é 2 elevado a k mais t, onde k é o número de dicas e t é o trabalho para desenvolver cada uma. É uma fórmula que parece rigorosa até você tentar colocar número nela, o que revela a intenção. Complexidade explode com cada insight extra necessário. Um problema que precisa de cinco saltos conceituais é ordens de magnitude mais difícil que um que precisa de dois, mesmo que o trabalho braçal seja parecido.

Outra característica crítica é que dicas têm ordem. A terceira dica só faz sentido depois que você suou nas duas primeiras e reformulou o problema. Isso quebra a ideia ingênua de força bruta, de listar mil técnicas matemáticas e testar todas as combinações. A busca percorre uma árvore. Cada insight inicial muda a representação do problema e revela quais caminhos passam a existir. Sem a reformulação certa, você nem consegue enxergar o próximo passo, por mais compute que tenha.

Busca humana versus busca da máquina

Humanos resolvem em largura. Geram direções candidatas, exploram raso, abandonam a maioria e apostam em poucas. Um pesquisador abandona uma ideia promissora se ela não dá sinal verde cedo, porque desenvolver custa meses de vida. Ele precisa de promessa conceitual, resultado parcial ou experiência passada para continuar. É uma restrição biológica e econômica, não lógica. A máquina não tem esse medo. Ela pode levar uma dica fraca adiante por muito mais passos, testar variações chatas, computar casos que um humano julgaria tediosos e manter dezenas de ramos vivos em paralelo sem cansar.

Na visão de operador, isso se traduz em arquitetura. Pense em um loop de agente com gerador de conjecturas, executor de código e verificador formal. A API não é só chamada ao modelo, é um pipeline com busca, avaliação e poda. O custo não está em um prompt gigante, está em milhares de rollouts, verificações em Lean ou Python, cálculo simbólico e reescrita. A latência por tentativa é baixa, mas o volume é alto. Minha inferência plausível é que esses resultados usam busca guiada por prova, com recompensa em verificação automática, não em julgamento humano. Onde dá para verificar por programa, a IA pode iterar sem supervisão. Onde a verificação exige intuição, ela ainda patina.

O que isso muda na prática

Quem ganha agora é quem tem problema verificável e espaço de construção grande. Combinatória, teoria dos números computacional, otimização discreta e formalização são terreno fértil. Quem perde é quem vende que matemática de ponta ainda é barreira humana garantida. Para laboratórios, universidades e times de pesquisa aplicada, a conta muda. Não dá mais para assumir que conjectura antiga é difícil por ser profunda, pode ser difícil só porque exige trabalho tedioso entre insights, exatamente o que a máquina faz bem.

• Se você pesquisa, mapeie seus problemas por verificabilidade antes de chamar a IA
• Se você constrói produto, trate prova formal como teste automatizado, não como luxo acadêmico
• Se você estuda, aprenda a dar bons hints e a avaliar construções, isso vale mais que decorar técnica

A ação prática mais direta é esta. Pegue um problema travado seu e reescreva como sequência de três dicas testáveis, com critério de verificação automática para cada etapa. Por exemplo, em vez de pedir para o modelo provar algo, peça para gerar contraexemplos parametrizados em código, com teste que roda em segundos. Conecte isso a um loop de busca com orçamento fixo de tokens e poda por falha rápida. Você vai descobrir em uma tarde se seu problema é do tipo que a IA já consegue mastigar ou se ele exige um salto representacional que ainda é humano.

Tensão: isso escala ou só move o gargalo?

Aqui fica minha dúvida real. Resolver problemas com k pequeno e t grande é perfeito para escala de compute, porque t pode ser paralelizado. Mas e quando k é grande, quando precisa de seis ou sete reformulações profundas em sequência? A fórmula diz que o custo explode exponencialmente, e compute sozinho não resolve árvore que se ramifica errado no início. A IA atual ainda depende de humanos para sugerir que existe um contraexemplo, ou para apontar a família certa de construções. Ela executa muito bem depois do primeiro insight não óbvio, mas quem gera esse primeiro insight fora da distribuição?

Tem também o custo que ninguém gosta de detalhar. Manter milhares de agentes provando, verificando e descartando ramos custa caro em inferência e em engenharia de avaliação. Funciona para um feito emblemático com time de elite e orçamento folgado. Funciona para rotina de P and D com prazo e margem apertada? Ainda não está claro. O risco é que a gente só tenha movido o gargalo, de fazer conta para formular bem o problema e construir o verificador confiável. E formular bem continua sendo trabalho humano, lento e mal pago.

Conclusão

A IA não ficou boa em toda a matemática, ficou muito boa em um tipo específico de matemática, aquela onde verificação é barata e trabalho tedioso conta mais que gênio isolado. A pergunta que fica é simples e prática. Qual problema seu tem verificador automático pronto para guiar a busca hoje?