Modelo Intern-S2 auxilia prova do caso 3D da conjectura de Ghys
Shanghai AI Laboratory relata que o modelo Intern-S2 contribuiu para provar o caso tridimensional da conjectura de Ghys, verificado em Lean.
Resumo rápido
- Intern-S2 ajudou a provar o caso 3D da conjectura de Ghys.
- A prova foi formalizada em Lean com 550 mil linhas de código.
- O código está disponível no GitHub e será transformado em módulo reutilizável.
Entenda o contexto
O Shanghai AI Laboratory desenvolve modelos de IA para apoiar pesquisas científicas. Intern-S2 é um modelo multimodal voltado a tarefas de descoberta, e o assistente Lean permite formalizar provas matemáticas de forma verificável.
O Shanghai AI Laboratory anunciou que seu modelo científico multimodal Intern-S2 colaborou na demonstração do caso tridimensional da conjectura de Ghys, problema de dinâmica complexa formulado em 1995.
Processo de descoberta com IA
Segundo a empresa, o Intern-S2 gerou um relatório inicial de 400 páginas e, ao longo de sete rodadas de interação, ampliou sua produção para cerca de mil páginas, enquanto seu grafo de problemas crescia de 15 para 389 nós. Os matemáticos, liderados por Disheng Xu e Jiesong Zhang, identificaram os pontos críticos, corrigiram a direção da argumentação e consolidaram a prova final.
A equipe da Universidade de Pequim, composta por Bin Dong e Ruochuan Liu, utilizou o assistente de teoremas Lean para formalizar os quatro principais teoremas do artigo, produzindo aproximadamente 550 000 linhas de código Lean com até 100 agentes rodando em paralelo. O código foi tornado público no GitHub.
O trabalho, descrito no artigo "Codimension-one holomorphic Anosov diffeomorphisms" publicado no arXiv em 29 de setembro e revisado em 13 de outubro, demonstra que toda difeomorfismo Anosov holomórfico de codimensão‑um em uma variedade complexa compacta e conexa é conjugado biholomorficamente a um automorfismo hiperbólico de um toro complexo, confirmando a conjectura em dimensão três.
O laboratório pretende empacotar todo o fluxo de trabalho como um módulo de verificação matemática reutilizável dentro de sua plataforma de descoberta científica, ampliando o potencial de IA em pesquisas avançadas.
Referências
- Fonte consultada: Pandaily — Tecnologia chinesa
Links para conferência: não indicam endosso das fontes ao conteúdo do portal.
Gostou? Compartilhe:
Comentários 0
Ninguém comentou ainda. Seja o primeiro!
