Prova da Conjectura de Freiman-Ruzsa Formalizada com IA

Terence Tao obteve sucesso na formalização da prova da conjectura polinomial de Freiman-Ruzsa usando uma ferramenta de IA, marcando um marco no uso generalizado da inteligência artificial na pesquisa matemática e causando grande impacto na comunidade matemática. Em seu blog, ele detalhou o processo de formalização da prova no Lean4 usando o Blueprint.

Este projeto, que durou três semanas, resultou na formalização bem-sucedida da prova da conjectura polinomial de Freiman-Ruzsa, demonstrando o incrível poder da inteligência artificial na pesquisa matemática.