IA encheu a matemática de lixo, então outra IA foi conferir tudo, linha por linha
Depois de 719 manuscritos não conferidos em um mês, uma startup de US$ 1,6 bilhão resolveu levar cada teorema ao computador para conferir
Enquanto a IA enche a matemática de artigos não conferidos (só a OpenAI soltou 719 manuscritos no mês passado), a Axiom Math, startup avaliada em US$ 1,6 bilhão, resolveu fazer o caminho inverso. Ela usou seus próprios agentes de IA para verificar formalmente o Stacks Project, uma das maiores bibliotecas de matemática do mundo, iniciada em 2005.
O time traduziu as cerca de 7.654 páginas em 16 milhões de linhas de código checadas pelo assistente de prova Lean. A empresa, fundada em março de 2025 pela CEO Carina Hong, 25 anos, levantou US$ 200 milhões em rodada Série A.