Terence Tao a réussi à formaliser la preuve de la conjecture polynomiale de Freiman-Ruzsa à l'aide d'un outil d'IA, marquant une avancée majeure dans l'application de l'intelligence artificielle à la recherche mathématique et suscitant une onde de choc au sein de la communauté mathématique.
Dans un billet de blog, il a détaillé le processus de formalisation de la preuve dans Lean4 en utilisant Blueprint. Ce projet, achevé en trois semaines, a abouti à la formalisation réussie de la preuve de la conjecture polynomiale de Freiman-Ruzsa, démontrant de manière impressionnante la puissance de l'intelligence artificielle dans la recherche mathématique.
