Aqui apresento uma auto-formalização completa de um artigo recente de matemática (novamente!) Barańczuk, Stefan. "Reduzindo o número de equações que definem um subconjunto do espaço n-dimensional sobre um corpo finito." Annales de la Faculté des sciences de Toulouse: Mathématiques, ser. 6, vol. 33, nº 1 (2024): 177–182. Passei alguns dias nesse projeto. Primeiro, rodei Aristóteles por @HarmonicMath , que em cerca de 15 horas formalizou completamente a demonstração. Então, com a grande ajuda de @PietroMonticone, consegui configurar uma versão blueprint da prova. Esta é uma versão em que todas as partes da documentação em LaTeX se tornam interativas e podem ser inspecionadas e estudadas. Podemos ver as dependências na prova e estudar suas relações. Na etapa de pós-processamento, também usei Grok Heavy e Codex CLI com GPT-5.2 em modo xhigh para escrever uma análise linha por linha da prova formal. Isso é uma grande ajuda para quem não é programador Lean 4 profissional. Você realmente pode internalizar todas as etapas da prova. Quero resumir minhas impressões e o que aprendi com essa experiência. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei