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.
Entre na conversa da comunidade