Nesta página colocarei alguns links para blogs, posts, entrevistas e outros sobre o assunto de Matemática e IA.
Terry Tao's blog : traz contribuições da comunidade matemática, além dos posts do próprio autor.
Proofs and Prompts : no ar desde agosto de 2026, este blog foi motivado pelos avanços recentes da IA em Matemática ("avanços" podem ser entendidos em mais de um sentido ...). Aceita contribuições de toda a comunidade matemática e tem publicações quase diárias. Em especial, tem muitas contribuições de estudantes e pesquisadores em início de carreira, que obviamente são os mais preocupados com a desestabilização provocada pela IA na área.
SAIR - Foundation for Science and AI Research , fundada por Terry Tao (entre outros). Aqui tem vários videos discutindo IA e ciência (não só matemática). Há competições feitas no estilo "ciência cidadã" ("citizen science"), mas com um pouquinho mais de exigência, em torno de questões abertas em matemática.
Anúncios de resultados
Open AI (27/10/2026) A conjetura de Kakeya foi provada para n = 3 por Hong Wang e Joshua Zahl em 2025, e Wang recebeu uma medalha Fields por este resultado. Há um explicação acessível sobre a conjetura neste artigo da Quanta. , e há este video muito acessível. Em 6/10, uma prova da conjetura de Kakeya para n = 4 fez parte da lista de 719 artigos da OpenAI. Agora, em 27/10, a OpenAI divulga uma prova da conjetura de Kakeya para todas as dimensões .
Open AI (6/10/2026) 722 719 artigos organizados em 372 famílias de resultados. Catálogo de resultados por área
Poucos dias depois, já começam a aparecer pequenos problemas. A OpenAI retirou 3 dos artigos por erros na prova. Além disso, uma conjetura listada aqui (artigo 208, "The finite Benson–Etingof–Ostrik conjecture" ) apareceu provada no arXiv em 2 de outubro ... e os autores desse último usaram uma versão do ChatGPT. Navier-Stokes novamente?
Menos da metade dos artigos foi checado pelo Lean -- e pior, agora sabe-se que isso não é garantia de correção, pois durante a tradução automática podem ser feitas correções que não são implementadas no artigo, o que pode levar a termos resultados corretos no Lean que não correspondem aos enunciados e provas originais. Vários exemplos são apresentados neste artigo sobre o artigo da OpenAI sobre Navier-Stokes.
É importante mencionar que nenhum dos problemas encontrados implica no artigo sobre Navier-Stokes ser invalidado. Na prática, o que esses problemas mostram é que, por enquanto, não é suficiente ter um artigo checado no Lean se a formalização no Lean foi feita por uma IA. No mesmo artigo sobre Navier-Stokes há um exemplo muito claro dos problemas enfrentados ao passar de um argumento em linguagem natural para uma versão formalizada no Lean. Ainda não estamos em uma situação de poder confiar tranquilamente em uma formalização automática via IA.