IA chinesa resolve problema matemático não resolvido há uma década em horas

Sistema de IA desenvolvido por pesquisadores da Universidade de Pequim resolveu, sem intervenção humana significativa, um problema matemático em aberto há mais de uma década (álgebra comutativa).
o feito foi descrito em um preprint publicado no repositório arXiv.
o modelo usa um framework de dois agentes: um para explorar estratégias de prova e outro para traduzir as soluções para uma linguagem formal verificável por máquinas.
a solução sintetizou décadas de literatura matemática e foi formalizada com validação automática, com pouca ou nenhuma intervenção humana.
o processo de verificação levou cerca de oitenta horas de computação, e a formalização ocorreu em poucas horas; a pesquisa não passou por revisão por pares ainda.

Um sistema de inteligência artificial desenvolvido por pesquisadores da Universidade de Pequim, na China, resolveu um problema matemático em aberto há mais de uma década, sem intervenção humana significativa. O estudo foi publicado como preprint no arXiv.

O desafio, iniciado em 2014 pelo matemático americano Dan Anderson, envolve álgebra comutativa. A solução foi alcançada com um modelo automatizado que opera sem supervisão humana direta.

O sistema usa um framework de dois agentes para chegar à resposta. Um agente explora estratégias e constrói provas; o outro as traduz para uma linguagem formal verificável por máquinas.

A abordagem combina raciocínio em linguagem natural com verificação formal, permitindo encontrar e validar soluções de forma automática, sem depender de intervenção constante.

Segundo os autores, o sistema sintetizou décadas de literatura matemática para resolver o problema e formalizar a prova com pouca ajuda humana, apenas ao fornecer documentos restritos.

A verificação completa exigiu cerca de 80 horas de computação, mas a formalização ocorreu em poucas horas, destacando a rapidez do método frente a especialistas humanos.

O estudo ainda não passou por revisão por pares, etapa comum na validação científica, mas os autores veem o resultado como exemplo concreto de automação na pesquisa matemática.

Desafios permanecem: provas matemáticas exigem rigor absoluto, e sistemas baseados em linguagem podem apresentar falhas ou inconsistências, segundo os pesquisadores.