OpenAI publica prova de conjectura matemática atribuída a IA

A prova transforma grafos em conjuntos de ciclos

A conjectura foi proposta por Tutte, Itai and Rodeh, Szekeres e Seymour. O PDF começa com uma redução atribuída a Jaeger: basta analisar grafos cúbicos sem loops. Essa etapa elimina parte da variedade de grafos sem mudar o problema central.

Em seguida, a prova usa o 8-flow theorem e um resultado de Tutte. Esses resultados permitem rotular cada aresta com um elemento não nulo de Γ = F32, um grupo em que a soma dos rótulos incidentes em cada vértice é zero. O texto trata esse rótulo como um fluxo nowhere-zero.

A etapa decisiva troca cada rótulo por um conjunto de dois elementos de Γ. A construção busca garantir que cada elemento apareça zero ou duas vezes nas três arestas ligadas a cada vértice. Parece uma condição local.

O argumento então transforma essa condição em uma cobertura global. Para cada elemento s de Γ, o conjunto de arestas que contém s tem grau zero ou dois em todos os vértices; por isso, forma uma união de ciclos. Como cada aresta pertence a exatamente dois desses conjuntos, os componentes dos ciclos formam um cycle double cover.

A prova não usa um contraexemplo nem uma estimativa experimental. Ela afirma um resultado para todos os grafos da classe definida pelo teorema. O texto também permite arestas paralelas e considera duas arestas paralelas como um ciclo, detalhe que afeta diretamente os casos tratados.

A disputa está na conferência de cada passo

A concisão do texto divide os leitores. ak_111 escreveu: “Ao contrário do unit distance problem, o impressionante aqui é que se trata de uma prova, e não de um contraexemplo.” O comentário também diz que a prova parece curta e elementar, embora isso não signifique que seja fácil, e identifica como desafio ainda não vencido pela IA a criação autônoma de uma teoria nova para atacar uma conjectura aberta.

A principal objeção não mira o uso de fluxos ou a álgebra linear. Ela mira a auditoria. nilkn escreveu: “Como isso não está em Lean e é extremamente fácil algo assim conter um erro sutil, eu preferiria que isso fosse anunciado por um matemático profissional.” Para ele, uma revisão independente deveria testar rapidamente uma prova curta, antes que textos plausíveis se multipliquem.

amazingamazing colocou o problema em termos de método: “Aqui temos uma afirmação de que a conjectura do double cover tem uma prova. Verificada por… ninguém, segundo o link.” O comentário pergunta como alguém descobriria um erro na prova e conclui que o próprio processo de verificação precisa acontecer antes de tratar o resultado como descoberta.

Os participantes concordam que a aparência formal não basta. A declaração do documento atribui a prova ao GPT 5.6 Sol Ultra, enquanto o Codex teria produzido o texto com GPT 5.6 Sol. Isso identifica o papel dos sistemas, mas não substitui a checagem de cada definição, redução e igualdade usada no argumento.

O debate também questiona como modelos recebem problemas difíceis. bgirard escreveu: “Tenho curiosidade sobre quantos problemas não resolvidos são testados contra modelos de fronteira quando eles são lançados. Estamos testando todos os problemas contra todas as versões?” A pergunta amplia o caso: além de validar uma prova, pesquisadores precisam decidir quais conjecturas testar e como distribuir esse trabalho.

O ponto em aberto é concreto: a construção dos conjuntos Pᵉ e a passagem dos rótulos locais para uma cobertura global precisam sobreviver à revisão matemática. Até essa checagem, o PDF registra uma afirmação forte e um caminho técnico específico, não um resultado aceito pela comunidade. Para equipes que usam IA em pesquisa, a consequência é direta: gerar uma prova e demonstrar que ela merece confiança são tarefas diferentes.