Um sistema de intelig\u00eancia artificial desenvolvido por pesquisadores da Universidade de Pequim, na China, resolveu um problema matem\u00e1tico em aberto h\u00e1 mais de uma d\u00e9cada, sem interven\u00e7\u00e3o humana significativa. O estudo foi publicado como preprint no arXiv.<\/p>\n
O desafio, iniciado em 2014 pelo matem\u00e1tico americano Dan Anderson, envolve \u00e1lgebra comutativa. A solu\u00e7\u00e3o foi alcan\u00e7ada com um modelo automatizado que opera sem supervis\u00e3o humana direta.<\/p>\n
O sistema usa um framework de dois agentes para chegar \u00e0 resposta. Um agente explora estrat\u00e9gias e constr\u00f3i provas; o outro as traduz para uma linguagem formal verific\u00e1vel por m\u00e1quinas.<\/p>\n
A abordagem combina racioc\u00ednio em linguagem natural com verifica\u00e7\u00e3o formal, permitindo encontrar e validar solu\u00e7\u00f5es de forma autom\u00e1tica, sem depender de interven\u00e7\u00e3o constante.<\/p>\n
Segundo os autores, o sistema sintetizou d\u00e9cadas de literatura matem\u00e1tica para resolver o problema e formalizar a prova com pouca ajuda humana, apenas ao fornecer documentos restritos.<\/p>\n
A verifica\u00e7\u00e3o completa exigiu cerca de 80 horas de computa\u00e7\u00e3o, mas a formaliza\u00e7\u00e3o ocorreu em poucas horas, destacando a rapidez do m\u00e9todo frente a especialistas humanos.<\/p>\n
O estudo ainda n\u00e3o passou por revis\u00e3o por pares, etapa comum na valida\u00e7\u00e3o cient\u00edfica, mas os autores veem o resultado como exemplo concreto de automa\u00e7\u00e3o na pesquisa matem\u00e1tica.<\/p>\n
Desafios permanecem: provas matem\u00e1ticas exigem rigor absoluto, e sistemas baseados em linguagem podem apresentar falhas ou inconsist\u00eancias, segundo os pesquisadores.<\/p>\n","protected":false},"excerpt":{"rendered":"