Anthropic publica formalização end-to-end do Último Teorema de Fermat em Lean 4 rodada por Claude — 11 dias, 30.300 teoremas e ~13 mi de linhas

Claude operou de forma majoritariamente autônoma pela plataforma Prove2Me (Columbia) durante 11 dias com dezenas de agentes paralelos, produziu ~13 milhões de linhas de Lean 4, provou 30.300 teoremas (29.500 aproveitados) e consumiu ~6 bilhões de tokens de output — a formalização final é cerca de 5× o tamanho do Mathlib inteiro.