O grupo de investigadores da Universidade de Pequim, na China, desenvolveu um sistema de IA capaz de resolver e verificar um problema matemático em aberto sem intervenção humana relevante. O estudo é apresentado em artigo preliminar disponível no arXiv.
O modelo combinou dois agentes: um de raciocínio informal para explorar estratégias e construir demonstrações, e outro de verificação formal que traduz as provas para um formato rigoroso verificável por máquina. A única intervenção humana foi o acesso a documentos restritos.
O problema abordado é de álgebra comutativa e foi proposto pelo matemático norte-americano Dan Anderson. A conclusão da verificação ocorreu em cerca de 80 horas de execução pelo sistema.
O desenvolvimento foi publicado num meio de divulgação e não passou ainda por revisão por pares. A equipa sublinha a potencial mobilização da IA para automatizar tarefas antes exigentes de colaboração entre especialistas.
Segundo os investigadores, a abordagem facilita a resolução de problemas complexos e reforça a validação de resultados em investigação matemática, ainda que com desafios de fiabilidade.
O projeto surge num contexto de crescimento de modelos de linguagem e de sistemas baseados em agentes aplicados à matemática, com empresas chinesas a intensificar a competição tecnológica global.
Entre na conversa da comunidade