El darrer teorema de Fermat —que no hi ha solucions enteres positives per a x^n + y^n = z^n quan n és més gran que 2— va trigar més de tres-cents anys a demostrar-se, fins que el matemàtic britànic Andrew Wiles en va publicar una prova el 1994-1995. Traduir aquesta prova, i tota la maquinària matemàtica que hi ha al darrere, a un llenguatge que un ordinador pugui verificar pas per pas —la «formalització»— és una tasca diferent i extremament laboriosa, que fins ara es considerava fora de l'abast de cap sistema d'intel·ligència artificial en un termini raonable.
Anthropic ha anunciat el 4 de setembre que un conjunt d'agents basats en Claude, coordinats a través de la plataforma de formalització matemàtica Prove2Me, ha completat la primera demostració íntegra i verificada per màquina del teorema en el llenguatge Lean 4. En onze dies de feina majoritàriament autònoma, els agents han generat 13 milions de línies de codi, han demostrat 30.300 teoremes auxiliars —dels quals 29.500 s'utilitzen en la prova final— i han consumit uns sis mil milions de testimonis de sortida. Anthropic afirma que la formalització fa servir únicament els tres axiomes estàndard de Lean i no conté cap pas omès, i n'ha publicat el codi obertament.
La notícia és rellevant perquè situa la IA generativa, per primer cop, com a eina capaç d'assumir una tasca de formalització matemàtica d'una escala i complexitat que els mateixos experts consideraven fora d'abast en aquest horitzó temporal. El matemàtic Kevin Buzzard, especialista en formalització a l'Imperial College de Londres, ha qualificat la fita d'«extraordinària» i ha dit que ha trigat molt menys temps del que els experts preveien; resultats com aquest reforcen l'ús d'assistents de demostració com Lean com a terreny de prova fiable per avaluar el raonament matemàtic dels models, perquè cada pas queda verificat automàticament, sense marge per a al·lucinacions.
Cal precisar que la formalització no és una demostració nova ni independent del teorema: reprodueix, traduït a un llenguatge verificable per màquina, l'argument que Wiles i Richard Taylor van publicar fa tres dècades, no en descobreix cap de nova. Tampoc és un procés totalment autònom: investigadors humans han hagut de dissenyar l'arquitectura de treball dels agents, dividir el problema en parts abordables i supervisar-ne el progrés, de manera que encara no es pot parlar d'una IA que demostri sola teoremes d'aquesta complexitat des de zero.