- A equipa da Universidade de Pequim desenvolveu uma IA capaz de resolver e verificar um problema de álgebra comutativa proposto pelo matemático norte‑americano Dan Anderson, com a verificação concluída em cerca de 80 horas.
- O sistema utiliza um agente de raciocínio em linguagem natural e um agente de verificação formal para transformar provas em formato matemático verificável por máquina.
- A intervenção humana limitou‑se a fornecer acesso a documentos restritos; não houve necessidade de julgamento matemático durante o processo.
- O estudo, ainda não revisto por pares, foi publicado preliminarmente no repositório arXiv.
- O trabalho insere‑se no avanço dos modelos de linguagem e de sistemas de agentes na investigação matemática, num contexto de maior visibilidade do sector na China (DeepSeek, Alibaba, ByteDance).
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