Modelo chinês de IA ajuda a provar a conjectura de Ghys em três dimensões, com verificação matemática em Lean

Um problema matemático de 1995 atinge um novo marco

Uma conjectura matemática proposta em 1995 deu origem a uma demonstração que abrange a dimensão complexa três, na sequência de uma colaboração entre matemáticos e o modelo Intern-S2 do Laboratório de IA de Xangai. Uma equipa da Universidade de Pequim traduziu então os quatro teoremas principais do artigo em demonstrações verificadas pelo Lean, um sistema informático concebido para verificar o raciocínio matemático.

O Laboratório de IA de Xangai anunciou o feito em 15 de outubro de 2026, atribuindo-o a uma equipa liderada por Disheng Xu, professor na Universidade de Great Bay e investigador visitante no laboratório. O artigo de investigação, Codimension-one holomorphic Anosov diffeomorphisms, indica Jiesong Zhang, da Universidade 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. A conjectura diz respeito a uma relação notável entre movimento e forma: se um espaço que permite um determinado tipo de movimento caótico tem necessariamente uma estrutura matemática muito ordenada.

O Intern-S2 ajudou a desenvolver ideias e argumentos através de trocas sucessivas com os investigadores. Zhang afirma, na sua declaração sobre a utilização de IA, que verificou de forma independente toda a matemática. A colaboração combinou exploração automática, discernimento humano e um processo separado de verificação formal.

O laboratório descreve o feito como a primeira utilização de um modelo chinês de IA para ajudar a resolver um problema matemático desta importância. O resultado concreto é um teorema de classificação, acompanhado de uma pré-publicação de acesso público e de código de formalização também disponibilizado publicamente.

O que a demonstração revela sobre movimento e forma

A conjectura de Ghys pertence à dinâmica complexa, o estudo da forma como os sistemas matemáticos mudam quando as suas coordenadas seguem as regras dos números complexos. Um número complexo tem duas componentes reais, pelo que a dimensão complexa três corresponde localmente a seis dimensões reais. O enquadramento é mais abstrato do que o de um objeto comum a deslocar-se numa sala.

Um sistema de Anosov combina, de forma precisa, estiramento e compressão. Com a repetição do movimento, algumas direções contraem-se enquanto outras se expandem. Pontos de partida próximos podem afastar-se rapidamente, gerando um comportamento caótico, apesar de a regra que determina cada passo ser exata.

Uma imagem útil é a de um processo repetido que estica e dobra uma forma. O sistema matemático estudado é muito mais restritivo: o estiramento e a contração têm de satisfazer condições uniformes, e o movimento tem de preservar a estrutura definida pelas coordenadas complexas.

Ghys conjecturou que estes sistemas em variedades complexas compactas deveriam ter uma descrição algébrica padrão. Uma variedade é um espaço que parece simples numa pequena vizinhança, mesmo que a sua forma global seja complicada. Neste contexto, a compacidade é uma condição matemática que impede o espaço de se prolongar indefinidamente.

O teorema de Zhang afirma que todo o difeomorfismo holomorfo de Anosov de codimensão um numa 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 numa transformação algébrica padrão, num 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. O principal resultado é que a dinâmica complicada impõe esta descrição geométrica ordenada.

Porque importa o âmbito exato

O artigo aborda o caso de codimensão um. Nestes sistemas, isso significa que uma das componentes de contração ou expansão tem dimensão complexa um. O teorema abrange esta família restrita em geral e resolve a conjectura na dimensão complexa três.

A conjectura mais abrangente de Ghys diz respeito a sistemas holomorfos de Anosov numa gama mais ampla de variedades complexas e descreve-os através de modelos algébricos padrão em espaços chamados infra-nilvariedades complexas. O resultado de Zhang dá uma resposta particularmente rígida para o caso estudado: um toro complexo e um automorfismo hiperbólico.

Para os matemáticos que trabalham neste caso, o teorema transforma o problema: em vez de identificar um espaço e um movimento desconhecidos, passam a estudar um modelo padrão. Uma mudança de coordenadas liga o sistema original a esse modelo, preservando a geometria complexa.

Xu estudava o problema há vários anos. Anteriormente, investigou o caso da dimensão três com o seu antigo orientador, Artur Avila, galardoado com a Medalha Fields. Xu e Zhang obtiveram mais tarde resultados parciais relacionados, publicados no Journal of the European Mathematical Society. O novo trabalho dá continuidade a essa atenção prolongada à mesma questão matemática.

De um teste das Olimpíadas a uma parceria de investigação

O papel do Intern-S2 surgiu na sequência de um resultado anterior do Intern-S1 nas Olimpíadas Chinesas de Matemática de 2025. Nesse ano, a comissão da Sociedade Chinesa de Matemática responsável pelas competições de matemática do ensino secundário organizou um teste de IA, convidando três modelos chineses a resolver problemas no mesmo limite de tempo dos concorrentes humanos.

O Intern-S1 obteve 102 pontos segundo os mesmos critérios de classificação, ficando em primeiro lugar entre os três modelos participantes. O limiar para a medalha de ouro era de 78 pontos, pelo que a pontuação ficou 24 pontos acima desse valor, ou cerca de 31% acima.

Xu viu potencial na utilização desta família de modelos em matemática de investigação, enquanto o Laboratório de IA de Xangai pretendia passar dos problemas de competição para questões por resolver. 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 suas trocas com os investigadores.

As principais etapas foram:

• 1995: Etienne Ghys propôs a conjectura.
• 2025: O Intern-S1 obteve 102 pontos no teste de IA das Olimpíadas Chinesas de Matemática.
• Início de 2026: Xu e o Laboratório de IA de Xangai iniciaram a colaboração de treino do modelo.
• Março de 2026: Xu tornou-se investigador visitante no laboratório.
• Agosto de 2026: Uma versão desenvolvida internamente do Intern-S2 e o sistema de apoio atingiram a fase utilizada para exploração matemática intensiva.
• 29 de setembro: O artigo de Zhang foi publicado no arXiv, seguindo-se uma revisão em 13 de outubro.
• 15 de outubro de 2026: O feito foi anunciado publicamente.

Como os matemáticos orientaram a IA

A primeira exploração do problema pelo Intern-S2 produziu um relatório de derivação com cerca de 400 páginas. Xu convidou Zhang, seu antigo aluno e investigador pós-doutorado na KTH, a juntar-se ao trabalho como investigador visitante. Zhang acompanhava a conjectura de Ghys desde o doutoramento.

Xu e Zhang analisaram as propostas do modelo, identificaram vias promissoras e deram feedback para orientar a exploração seguinte. A máquina explorou linhas de raciocínio e gerou argumentos; os matemáticos decidiram que direções mereciam mais trabalho e ajudaram a reunir a demonstração final.

O laboratório descreve sete rondas de raciocínio continuado. Durante o processo, o grafo do problema do modelo cresceu de 15 para 389 nós, enquanto o resultado acumulado chegou a cerca de mil páginas e incluiu dezenas de abordagens propostas.

Um grafo de problema é um mapa de tarefas matemáticas mais pequenas e das ligações entre elas. Um nó pode representar uma afirmação intermédia, enquanto outro representa um resultado necessário para a demonstrar. O aumento referido mostra até que ponto o sistema dividiu e explorou o problema.

A declaração de Zhang sobre a utilização de IA explica diretamente a responsabilidade pela matemática final: uma versão interna do Intern-S2 ajudou a desenvolver ideias e argumentos através de várias rondas de diálogo, e Zhang verificou a matemática de forma independente. No artigo, agradece também a Xu pelas discussões continuadas.

O contributo do software de apoio

O Laboratório de IA de Xangai associou o modelo a um software destinado a gerir longas cadeias de raciocínio e o feedback humano repetido. O sistema podia dividir uma questão difícil em tarefas mais pequenas, explorar várias direções e apresentar resultados para avaliação dos investigadores.

A abordagem de treino combinou conhecimentos científicos abrangentes com materiais orientados para a matemática de investigação, incluindo problemas difíceis retirados de artigos matemáticos e métodos para verificar soluções propostas. O laboratório refere também a utilização de aprendizagem por reforço com recompensas verificáveis, o que significa que o raciocínio bem-sucedido e verificável podia servir de sinal de treino.

Os investigadores utilizaram depois a experiência obtida com o sistema de apoio para melhorar o próprio modelo. O objetivo prático era manter progressos úteis ao longo de uma investigação prolongada, incluindo acompanhar resultados intermédios e corrigir erros à medida que surgiam novos argumentos.

O laboratório citou ainda resultados no IMO-Proof e no AdvancedMathBench, avaliações centradas no raciocínio matemático. No projeto de Ghys, a prova mais detalhada do funcionamento do sistema é a sequência de extensas derivações, feedback de especialistas, um artigo concluído e a posterior verificação formal.

Como a Universidade de Pequim verificou a demonstração

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

A formalização traduz definições, pressupostos e raciocínios matemáticos para uma linguagem que um computador consegue verificar. Um artigo convencional pode contar com um leitor experiente para completar passos familiares. O Lean exige que esses passos sejam expressos através de afirmações precisas e operações lógicas permitidas.

Os membros da equipa Jiedong Jiang e Bin Wu afirmaram que o trabalho demorou cerca de cinco dias, com até 100 agentes de IA a operar em paralelo. Foram produzidas aproximadamente 550 000 linhas de código Lean. Os especialistas verificaram também se as afirmações formalizadas correspondiam ao significado matemático dos teoremas principais do artigo.

O SHEAF organizou a tarefa como um grafo direcionado de definições, proposições e dependências. Isso permitiu que diferentes agentes trabalhassem em partes relacionadas, enquanto a equipa acompanhava quais as afirmações já demonstradas 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 existiam nas bibliotecas de matemática formal disponíveis. A equipa teve de estabelecer essas bases ou encontrar formas de recorrer a resultados existentes e, depois, ligar as várias partes numa cadeia completa.

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

Porque as duas etapas se complementam

O Intern-S2 e o SHEAF tiveram funções diferentes. O primeiro apoiou a procura de ideias e argumentos matemáticos. O segundo ajudou a construir demonstrações formais que o Lean podia verificar. Os matemáticos orientaram a exploração, verificaram a matemática resultante e avaliaram se as afirmações formalizadas correspondiam aos teoremas pretendidos.

A escala do trabalho torna concreta esta divisão. Cerca de mil páginas de resultados exploratórios serviram de base a um artigo de investigação; o processo de verificação gerou depois cerca de 550 000 linhas de código formal. Cada etapa transformou o trabalho numa forma diferente, adequada a uma tarefa distinta.

Para futuros investigadores, o artigo público apresenta o argumento matemático, enquanto o código público regista a estrutura da demonstração formal. As definições e os resultados auxiliares acrescentados durante a formalização também poderão servir de ponto de partida para trabalhos posteriores na mesma área.

O próximo passo é criar um módulo de verificação reutilizável

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

O laboratório tenciona também aplicar a outras disciplinas com estruturas matemáticas relacionadas as capacidades de raciocínio desenvolvidas neste projeto. O ciclo proposto consiste em resolver um problema de investigação, transformar métodos úteis em software reutilizável e aplicá-los a outra investigação.

Para Xu, o resultado prolonga um interesse de investigação de longa data através da colaboração entre a Universidade de Great Bay, 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 como um exemplo detalhado da participação da IA na investigação sob orientação humana.

Pontos principais

• A nova demonstração 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 investigação e afirma ter verificado de forma independente toda a matemática.
• Disheng Xu e Zhang orientaram o Intern-S2 através de ciclos repetidos de exploração e feedback.
• O grafo do problema do modelo cresceu 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 os quatro teoremas principais e os resultados auxiliares.
• O processo de verificação terá demorado cerca de cinco dias e gerado aproximadamente 550 000 linhas de código.
• O laboratório planeia transformar o fluxo de trabalho num módulo de verificação matemática reutilizável.