Uma conjectura de trinta anos, um modelo chinês e uma prova verificada por máquina

Uma conjectura de trinta anos, um modelo chinês e uma prova verificada por máquina

Em 15 de outubro, o Shanghai AI Laboratory (上海人工智能实验室) anunciou que uma equipe de pesquisa havia provado o caso tridimensional da conjectura de Ghys, um problema em aberto em sistemas dinâmicos que resiste desde 1995. O trabalho foi desenvolvido com o Intern-S2, o modelo próprio do laboratório, e a prova final foi verificada formalmente em Lean por uma equipe da Peking University (北京大学).

A relevância não está apenas no fato de um problema difícil ter caído. Está em que o anúncio foi estruturado em torno de um processo e não de um número: um modelo que produz derivações, pesquisadores que escolhem em quais linhas de ataque concentrar atenção e um assistente de provas que certifica cada passo. Essa combinação é o que o setor promete há dois anos, e aqui está ela, com um artigo anexado.

O que a conjectura pergunta

Étienne Ghys propôs o problema em 1995. Em termos gerais, pergunta se o comportamento de sistemas dinâmicos caóticos pode determinar sua classificação geométrica, o que equivale a perguntar se o movimento revela a forma do espaço em que ocorre.

O que foi resolvido não é a questão geral. A equipe provou o caso de codimensão um, ou seja, o cenário tridimensional, que permanecia em aberto havia três décadas. Essa distinção importa para ler a afirmação com honestidade: a conjectura completa continua mais ampla, mas o caso específico que resistia a todos até agora está encerrado.

A primeira passagem produziu quatrocentas páginas

A mecânica da colaboração é mais interessante do que o resultado, porque mostra como a pesquisa humano-IA realmente se parece minuto a minuto.

A primeira exploração do problema pelo Intern-S2 produziu um relatório de derivação de cerca de 400 páginas. Isso não é uma resposta. É um monte de raciocínio candidato, parte útil e parte não, que é exatamente a forma de saída que se obtém quando se pede a um modelo que pense em algo genuinamente não resolvido em vez de recordar algo conhecido.

A partir daí, o trabalho passou por sete rodadas de raciocínio continuado. O grafo do problema, um mapa de subafirmações e de como dependem umas das outras, cresceu de 15 para 389 nós. A produção acumulada chegou a cerca de mil páginas e incluiu dezenas de abordagens distintas. Em cada etapa, os matemáticos fizeram o que o modelo não consegue fazer sozinho: examinaram as propostas, decidiram quais aberturas eram promissoras e orientaram a rodada seguinte.

Xu Disheng, pesquisador visitante no laboratório e professor na Greater Bay University, e Zhang Jiesong, pesquisador de pós-doutorado que acompanha a conjectura desde o doutorado, forneceram esse julgamento. O artigo de Zhang, publicado no arXiv em 29 de setembro e revisado em 13 de outubro, é um trabalho de autor único com uma declaração de uso de IA: o modelo ajudou a desenvolver as ideias e os argumentos em múltiplas rodadas de diálogo, e ele verificou a matemática de forma independente.

A parte que o torna mais do que uma história

Afirmações de que a IA resolve matemática são baratas. O que dá peso a esta é que a prova foi formalizada.

A equipe da Peking University, liderada por Bin Dong e Ruochuan Liu, usou seu próprio framework SHEAF para formalizar todos os quatro teoremas principais, além dos resultados de apoio de Ghys dos quais os argumentos dependem. Formalizar significa traduzir definições, suposições e raciocínio para uma linguagem que um computador possa checar, onde cada passo do argumento do autor precisa ser escrito explicitamente em vez de ser deixado para um leitor treinado completar.

O esforço levou cerca de cinco dias, com até 100 agentes trabalhando em paralelo, e produziu aproximadamente 550 mil linhas de código Lean. Lean é um provador de teoremas interativo. Ele não se importa com o quanto alguém se sente confiante. Ele checa a lógica e aceita a prova ou não aceita.

O SHEAF organizou a tarefa como um grafo direcionado de definições, proposições e dependências, de modo que agentes separados pudessem trabalhar em peças conectadas enquanto a equipe acompanhava quais afirmações tinham prova e quais ainda precisavam dela. Esse é um tipo genuinamente novo de divisão do trabalho, e o framework também teve de preencher lacunas na biblioteca formal existente para sistemas dinâmicos, porque a maquinaria de que essa prova precisava simplesmente ainda não existia.

Humanos e modelo, tarefas diferentes

A divisão do trabalho descrita pelo laboratório merece ser tomada ao pé da letra, porque não é a versão lisonjeira para nenhum dos lados.

O modelo vasculhou a literatura, quebrou a proposição em pedaços, explorou ramos de prova em paralelo, checou passos lógicos e testou um grande número de ideias rapidamente. Os humanos definiram a direção, julgaram quais abordagens valia a pena perseguir e tomaram as decisões que determinavam onde gastar o esforço da rodada seguinte.

Nenhuma das metades se parece com a outra. A contribuição do modelo é escala e fôlego: ele consegue manter dezenas de becos sem saída na memória sem se desanimar. A contribuição dos humanos é o gosto, ou seja, a capacidade de olhar cem páginas de raciocínio plausível e saber quais três parágrafos importam.

Há uma anedota ligada a isso, da qual a imprensa chinesa fez grande alarde. Um especialista em sistemas dinâmicos teria submetido o mesmo problema ao GPT-6 por curiosidade, depois de ouvir que um modelo nacional o havia resolvido, e ele não chegou lá. Lido estritamente, é uma comparação entre dois sistemas em um problema, o que prova muito pouco. Lido como um sinal sobre a dinâmica competitiva, é o tipo de detalhe que move investimentos.

Por que a verificação formal muda o que está em jogo

Durante a maior parte dos últimos dois anos, o gargalo da matemática assistida por IA não foi gerar argumentos candidatos. Os modelos são bons em produzir raciocínio plausível. O gargalo foi saber qual parte disso está correta, porque checar uma prova é lento, exige especialistas e não se paraleliza bem.

O Lean inverte isso. Uma vez que um enunciado é formalizado, a verificação fica barata e rápida, e pode ser confiada porque é mecânica em vez de social. As 550 mil linhas são a parte cara, e o fato de uma equipe mais cem agentes terem conseguido produzi-las em cinco dias é o verdadeiro avanço aqui. Isso sugere que o gargalo da verificação pode estar se afrouxando justamente quando o da geração já estava solto.

O laboratório diz que vai empacotar o fluxo de trabalho como um módulo reutilizável de verificação matemática em sua plataforma de descoberta científica, conectando o modelo, os agentes, os dados e o equipamento experimental. Também cita um resultado anterior, no qual uma equipe da Wuhan University (武汉大学) usou a plataforma para reduzir o ciclo de desenvolvimento de uma síntese eletroquímica de cinco a dez anos para um a dois.

O que tirar disso

O resumo honesto é que este é um resultado real com uma prova real, produzido por um fluxo de trabalho que ainda é muito intensivo em pessoas. Sete rodadas de orientação especializada não são um modelo rodando sozinho. Um artigo de autor único com declaração de uso de IA não é um modelo reivindicando crédito.

O que mudou é que agora o ciclo se fecha. Um modelo consegue produzir raciocínio suficiente para importar em um problema que ninguém resolveu, os humanos conseguem direcioná-lo, e um assistente de provas consegue certificar o resultado sem que ninguém precise confiar em um resumo. Isso é um pipeline, não uma demo, e são os pipelines que transformam uma capacidade em uma prática.

A próxima pergunta é se isso se generaliza além dos casos em que a formalização é sequer possível. Geometria e dinâmica têm alguma estrutura que se presta à checagem por máquina. Boa parte do resto da ciência não tem, e é nesse território mais bagunçado, na biologia, nos materiais e na medicina, que a promessa da IA como assistente de pesquisa será realmente testada. O resultado de Ghys diz que a ferramenta pode funcionar. Ainda não diz com que frequência.