UMA IA DECIFRA UM ENIGMA DE COLORAÇÃO

Pegue uma rede de pontos ligados por linhas — o que os matemáticos chamam de grafo. Agora pinte os pontos de modo que dois pontos ligados por uma linha nunca tenham a mesma cor. O menor número de cores que funciona é o número cromático do grafo. Um caso particular famoso é o teorema das quatro cores, provado em 1977, cujo título diz tudo: “Every planar map is four colorable” (todo mapa plano pode ser colorido com quatro cores).

A aposta de Hadwiger em 1943

Em 1943, Hadwiger propôs uma regra abrangente para todos os grafos. Reduza um grafo apagando pontos ou linhas e fundindo dois pontos ligados num só. O resultado se chama menor (minor). Hadwiger olhou para o maior grafo completo — um aglomerado em que cada ponto está ligado a todos os outros — que se pode obter dessa forma, e conjecturou que o número de cores necessário nunca ultrapassa o tamanho desse aglomerado.

O artigo o chama de “um dos problemas mais antigos e fundamentais da teoria dos grafos”. Ele só está provado para casos pequenos: aglomerados de até cinco pontos, em que se mostra equivalente ao teorema das quatro cores ou redutível a ele. A partir de seis, está em aberto.

Chegando perto, um logaritmo de cada vez

Como o enunciado exato resiste, os pesquisadores tentaram limitar o número de cores por alguma função do tamanho do aglomerado, que cresça o mais devagar possível. O artigo relata os avanços. Durante décadas, o melhor limite cresceu um pouco mais rápido que proporcionalmente — por um fator envolvendo a raiz quadrada de um logaritmo. Há alguns anos, Norin, Postle e Song quebraram essa barreira. Delcourt e Postle o melhoraram ainda mais e, crucialmente, mostraram que basta lidar com grafos razoavelmente pequenos. Liu e Luo empurraram o fator extra para baixo, até um logaritmo triplo.

O ponto de chegada natural é a conjectura linear de Hadwiger: um múltiplo fixo do tamanho do aglomerado sempre basta. É isso que Sergey Norin, da Universidade McGill, em Montreal, e Raphael Steiner, da ETH Zurique, agora afirmam provar.

O papel da máquina

Os autores são explícitos: a prova foi encontrada pelo GPT-6 Astra, um modelo da OpenAI, seguindo as orientações deles. Primeiro, pediram que ele provasse o caso dos grafos muito densos, que eles acreditavam ser a peça que faltava. Ele conseguiu, escrevem, “depois de apenas algumas horas e algum encorajamento”. Quando lhe pediram para tornar explícita uma dependência, ele cobriu grafos até certo tamanho — mas não exatamente o intervalo necessário. Então pediram uma ideia original para fechar a lacuna, o que produziu a etapa de “bootstrap” da prova final. Quase nenhuma das ideias de prova específicas dos próprios autores sobreviveu, dizem eles, exceto uma sugestão sobre contrações.

A redação é humana. Outro modelo da OpenAI ajudou na revisão do texto e na bibliografia. Os autores relatam que o Codex, da OpenAI, produziu uma versão formal, verificável por máquina, da prova inteira no assistente de provas Lean, publicada online junto com um rascunho inicial escrito por IA. Eles assumem total responsabilidade pela matemática.

Por dentro da prova

O argumento tem duas metades:

1. Grafos pequenos, poucas cores. Para grafos não muito maiores que o limite do aglomerado, os autores mostram que cerca de quatro vezes o tamanho do aglomerado basta. O ponto de partida é um resultado de Reed e Seymour, de 1998: uma forma relaxada, “fracionária”, de coloração já obedece à regra linear com fator dois. O novo trabalho transforma colorações fracionárias em colorações reais acrescentando algumas linhas extras ao grafo e encontrando emparelhamentos enormes numa estrutura auxiliar.
2. Um bootstrap. Um segundo argumento amplia o intervalo de tamanhos de grafo coberto por um fator de quatro terços no expoente a cada etapa, ao custo de uma constante maior. Dez etapas levam o intervalo de um terço a cerca de 5,92, além do limiar de 5 exigido pela redução de Delcourt-Postle. Essa metade usa um velho truque devido a Gyárfás, que, segundo os autores, nunca havia sido aplicado a esse problema.

Os autores descrevem a prova como construída com ferramentas conhecidas — “contida no fecho convexo dos resultados existentes”, mas não numa borda óbvia dele.

O que continua em aberto

A constante é enorme: uma estimativa grosseira dá cerca de 10¹⁰⁰. Os autores veem espaço para trazê-la abaixo de 10¹⁰, mas acham que chegar, digamos, a 100 exigiria ideias novas. A conjectura exata de Hadwiger fica intocada: “Estamos indecisos”, escrevem. O artigo é um preprint; 41 páginas de matemática nova agora vão enfrentar o escrutínio de outros especialistas.