Modelo chinês de IA ajuda a provar conjectura de Ghys em três dimensões, com a matemática verificada pelo Lean

Problema matemático de 1995 alcança um novo marco

Uma conjectura matemática proposta em 1995 teve sua prova estabelecida para a dimensão complexa três, após uma colaboração entre matemáticos e o modelo Intern-S2, do Laboratório de IA de Xangai. Em seguida, uma equipe da Universidade de Pequim traduziu os quatro principais teoremas do artigo em provas verificadas pelo Lean, um sistema computacional desenvolvido para verificar o raciocínio matemático.

O Laboratório de IA de Xangai anunciou o resultado em 15 de outubro de 2026 e o atribuiu a uma equipe liderada por Disheng Xu, professor da Universidade da Grande Baía e pesquisador visitante no laboratório. O artigo de pesquisa, Codimension-one holomorphic Anosov diffeomorphisms, lista Jiesong Zhang, do Instituto Real de Tecnologia KTH, da Suécia, como único autor.

O resultado resolve o caso de codimensão um da conjectura do matemático francês Etienne Ghys, incluindo o caso da dimensão complexa três. Trata-se de uma relação marcante entre movimento e forma: se um espaço que permite um tipo específico de movimento caótico precisa ter, em si, uma estrutura matemática altamente ordenada.

O Intern-S2 ajudou a desenvolver ideias e argumentos em trocas sucessivas com os pesquisadores. Zhang afirma em sua declaração sobre o uso de IA que verificou toda a matemática de forma independente. A colaboração combinou exploração por máquina, avaliação humana e um processo separado de verificação formal.

O laboratório descreve o resultado como a primeira vez que um modelo chinês de IA ajudou a resolver um problema matemático desse nível. O resultado concreto é um teorema de classificação, acompanhado de uma pré-publicação disponível ao público e de código de formalização também liberado publicamente.

O que a prova diz sobre movimento e forma

A conjectura de Ghys pertence à dinâmica complexa, área que estuda como sistemas matemáticos mudam quando suas coordenadas seguem as regras dos números complexos. Um número complexo tem duas componentes reais, então a dimensão complexa três corresponde localmente a seis dimensões reais. O cenário é mais abstrato do que o movimento de um objeto comum dentro de um cômodo.

Um sistema de Anosov combina, de maneira precisa, alongamento e compressão. Com o movimento repetido, algumas direções se contraem, enquanto outras se expandem. Pontos de partida próximos podem se afastar rapidamente, produzindo comportamento caótico, embora a regra que governa cada etapa seja exata.

Uma imagem útil é a de um processo repetido que estica e dobra uma forma. O sistema matemático estudado aqui é muito mais restritivo: o alongamento e a contração precisam satisfazer condições uniformes, e o movimento deve preservar a estrutura fornecida pelas coordenadas complexas.

Ghys propôs que esses sistemas em variedades complexas compactas deveriam ter uma descrição algébrica padrão. Uma variedade é um espaço que parece simples em uma vizinhança pequena, mesmo quando sua forma completa é complexa. Nesse contexto, a compacidade é uma condição matemática que impede o espaço de se estender indefinidamente.

O teorema de Zhang afirma que todo difeomorfismo holomorfo de Anosov de codimensão um em uma variedade complexa compacta e conexa é biholomorficamente conjugado a um automorfismo hiperbólico de um toro complexo. Em termos mais simples, uma mudança reversível de coordenadas que respeita a estrutura complexa transforma o movimento em uma transformação algébrica padrão em um espaço muito regular.

Um toro complexo pode ser construído identificando pontos do espaço complexo que diferem por elementos de uma rede periódica. A principal descoberta é que a dinâmica complexa impõe essa descrição geométrica ordenada.

Por que o escopo exato importa

O artigo aborda o caso de codimensão um. Para esses sistemas, isso significa que uma das partes contráteis ou expansivas tem dimensão complexa um. O teorema abrange essa família restrita de modo geral e resolve a conjectura na dimensão complexa três.

A conjectura mais ampla de Ghys trata de sistemas holomorfos de Anosov em uma variedade maior de variedades complexas e os descreve por meio de modelos algébricos padrão em espaços chamados infra-nilvariedades complexas. Para o caso estudado, o resultado de Zhang oferece uma resposta particularmente rígida: um toro complexo e um automorfismo hiperbólico.

Para os matemáticos que trabalham nesse caso, o teorema muda o problema: em vez de identificar um espaço e um movimento desconhecidos, passa-se a estudar um modelo padrão. Uma mudança de coordenadas conecta o sistema original a esse modelo, preservando a geometria complexa.

Xu estudava o problema havia anos. Anteriormente, investigou o caso da dimensão três com seu ex-orientador, Artur Avila, laureado com a Medalha Fields. Mais tarde, Xu e Zhang obtiveram resultados parciais relacionados, publicados no Journal of the European Mathematical Society. O novo trabalho se apoia nessa dedicação contínua à mesma questão matemática.

De uma olimpíada a uma parceria de pesquisa

O papel do Intern-S2 veio após um resultado anterior do Intern-S1 na Olimpíada Chinesa de Matemática de 2025. Naquele ano, a comissão da Sociedade Chinesa de Matemática responsável pelas competições de matemática do ensino médio organizou uma prova de IA e convidou três modelos chineses a resolver problemas no mesmo limite de tempo dos participantes humanos.

O Intern-S1 fez 102 pontos segundo os mesmos critérios de avaliação e ficou em primeiro lugar entre os três modelos participantes. A nota mínima para a medalha de ouro era 78 pontos, o que deixou o resultado 24 pontos acima desse patamar, ou cerca de 31% a mais.

Xu viu potencial no uso dessa família de modelos em pesquisas matemáticas, enquanto o Laboratório de IA de Xangai queria passar de problemas de competição a questões ainda sem solução. A colaboração começou no início de 2026 e incluiu a criação de um sistema de software, descrito como um Harness, para organizar o trabalho do modelo e as trocas com os pesquisadores.

As principais etapas foram:

• 1995: Etienne Ghys propôs a conjectura.
• 2025: O Intern-S1 fez 102 pontos na prova de IA da Olimpíada Chinesa de Matemática.
• Início de 2026: Xu e o Laboratório de IA de Xangai iniciaram a colaboração de treinamento do modelo.
• Março de 2026: Xu tornou-se pesquisador visitante no laboratório.
• Agosto de 2026: Uma versão desenvolvida internamente do Intern-S2 e seu sistema de suporte chegaram à etapa usada para exploração matemática intensiva.
• 29 de setembro: O artigo de Zhang foi publicado no arXiv, seguido de uma revisão em 13 de outubro.
• 15 de outubro de 2026: O resultado foi anunciado publicamente.

Como os matemáticos orientaram a IA

A primeira exploração do problema pelo Intern-S2 gerou um relatório de derivação com cerca de 400 páginas. Xu convidou Zhang, seu ex-aluno e pesquisador de pós-doutorado na KTH, para participar do trabalho como pesquisador visitante. Zhang acompanhava a conjectura de Ghys desde o doutorado.

Xu e Zhang examinaram as propostas do modelo, identificaram caminhos promissores e deram feedback para orientar as explorações seguintes. A máquina percorreu linhas de raciocínio e gerou argumentos; os matemáticos decidiram quais direções mereciam mais trabalho e ajudaram a montar a prova final.

O laboratório descreve sete ciclos de raciocínio contínuo. Durante o processo, o grafo do problema criado pelo modelo passou de 15 para 389 nós, enquanto o material acumulado chegou a cerca de mil páginas e incluiu dezenas de abordagens propostas.

Um grafo do problema é um mapa de tarefas matemáticas menores e das conexões entre elas. Um nó pode representar uma afirmação intermediária, enquanto outro representa um resultado necessário para demonstrá-la. O aumento relatado mostra a extensão com que o sistema dividiu e explorou o problema.

A declaração de Zhang sobre o uso de IA explica diretamente quem é responsável pela matemática concluída: uma versão interna do Intern-S2 ajudou a desenvolver ideias e argumentos em várias rodadas de diálogo, e ele verificou a matemática de forma independente. Em seu artigo, ele também agradece a Xu pelas discussões contínuas.

O que o software de apoio acrescentou

O Laboratório de IA de Xangai combinou o modelo com um software criado para gerenciar longas cadeias de raciocínio e feedback humano repetido. O sistema podia dividir uma questão difícil em tarefas menores, explorar várias direções e apresentar resultados para avaliação dos pesquisadores.

A abordagem de treinamento combinou conhecimentos científicos amplos com materiais voltados à matemática de pesquisa, incluindo problemas difíceis extraídos de artigos matemáticos e métodos para verificar soluções propostas. O laboratório também descreve o uso de aprendizado por reforço com recompensas verificáveis, ou seja, raciocínios bem-sucedidos e verificáveis podiam servir como sinal de treinamento.

Em seguida, os pesquisadores usaram a experiência com o sistema de apoio para melhorar o próprio modelo. O objetivo prático era manter avanços úteis ao longo de uma investigação prolongada, acompanhando resultados intermediários e corrigindo erros à medida que novos argumentos surgiam.

O laboratório também citou resultados nas avaliações IMO-Proof e AdvancedMathBench, voltadas ao raciocínio matemático. No projeto de Ghys, as evidências mais detalhadas sobre o funcionamento do sistema são a sequência de derivações extensas, o feedback dos especialistas, o artigo concluído e a verificação formal posterior.

Como a Universidade de Pequim verificou a prova

A equipe da Universidade de Pequim, liderada por Bin Dong e Ruochuan Liu, usou a estrutura SHEAF para formalizar os quatro principais teoremas do artigo de Zhang. O trabalho também abrangeu resultados de Ghys dos quais os argumentos dependem.

A formalização traduz definições, hipóteses e raciocínios matemáticos para uma linguagem que um computador pode verificar. Um artigo convencional pode depender de um leitor experiente para completar etapas conhecidas. O Lean exige que essas etapas sejam expressas por meio de afirmações precisas e operações lógicas permitidas.

Os integrantes da equipe Jiedong Jiang e Bin Wu disseram que o trabalho levou cerca de cinco dias, com até 100 agentes de IA operando em paralelo. O processo produziu aproximadamente 550 mil linhas de código Lean. Especialistas também verificaram se as afirmações formais correspondiam ao sentido matemático dos principais teoremas do artigo.

A SHEAF organizou a tarefa como um grafo direcionado de definições, proposições e dependências. Isso permitiu que diferentes agentes trabalhassem em partes conectadas, enquanto a equipe acompanhava quais afirmações já tinham provas e quais ainda precisavam de trabalho.

A formalização exigiu mais do que traduzir os argumentos finais. Alguns resultados auxiliares de dinâmica não estavam disponíveis nas bibliotecas de matemática formal existentes. A equipe precisou fornecer essa base ou encontrar caminhos que usassem resultados já disponíveis e, depois, conectar as partes em uma cadeia completa.

O artigo está disponível como pré-publicação no arXiv, e o código de formalização foi liberado no GitHub. O anúncio não especificou publicação em revista científica nem decisão de revisão por pares.

Por que as duas etapas se complementam

O Intern-S2 e a SHEAF cumpriram funções diferentes. O primeiro ajudou a buscar ideias e argumentos matemáticos. A segunda contribuiu para construir provas formais que o Lean pudesse verificar. Os matemáticos orientaram a exploração, conferiram a matemática resultante e avaliaram se as afirmações formais representavam os teoremas pretendidos.

A escala do trabalho deixa essa divisão clara. Cerca de mil páginas de material exploratório deram origem a um artigo de pesquisa; em seguida, o processo de verificação gerou aproximadamente 550 mil linhas de código formal. Cada etapa transformou o trabalho em um formato diferente, adequado a uma tarefa específica.

Para pesquisadores que vierem a trabalhar no tema, o artigo público apresenta o argumento matemático, enquanto o código público registra a estrutura da prova formal. As definições e os resultados auxiliares acrescentados durante a formalização também podem servir de ponto de partida para trabalhos posteriores na mesma área.

Próxima etapa é criar um módulo de verificação reutilizável

O Laboratório de IA de Xangai planeja transformar o fluxo de trabalho em um módulo de verificação matemática para a plataforma de descoberta científica Intern Duanyan. O objetivo é permitir que projetos posteriores reutilizem a combinação de exploração pelo modelo, feedback de especialistas e verificação formal.

O laboratório também pretende aplicar a outros campos com estruturas matemáticas relacionadas os recursos de raciocínio desenvolvidos por meio deste projeto. O ciclo proposto é resolver um problema de pesquisa, transformar métodos úteis em software reutilizável e aplicá-los a outra investigação.

Para Xu, o resultado amplia um interesse de pesquisa de longa data por meio da colaboração entre a Universidade da Grande Baía, o Laboratório de IA de Xangai, a KTH e a Universidade de Pequim. Para a comunidade matemática em geral, oferece tanto um novo resultado de classificação quanto um exemplo detalhado de participação da IA em pesquisas sob orientação humana.

Principais pontos

• A nova prova resolve o caso de codimensão um da conjectura de Ghys, incluindo a dimensão complexa três.
• Jiesong Zhang é o único autor do artigo de pesquisa e afirma ter verificado toda a matemática de forma independente.
• Disheng Xu e Zhang orientaram o Intern-S2 em rodadas sucessivas de exploração e feedback.
• O grafo do problema criado pelo modelo passou de 15 para 389 nós, com cerca de mil páginas de derivações.
• A estrutura SHEAF, da Universidade de Pequim, ajudou a formalizar no Lean quatro teoremas principais e resultados auxiliares.
• Segundo o relato, a verificação levou cerca de cinco dias e gerou aproximadamente 550 mil linhas de código.
• O laboratório planeja transformar o fluxo de trabalho em um módulo reutilizável de verificação matemática.