Aqui apresento uma auto-formalização completa de um recente artigo de matemática (novamente!) Barańczuk, Stefan. "Reduzindo o Número de Equações que Definem um Subconjunto do n-Espaço sobre um Campo Finito." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Passei alguns dias neste projeto. Primeiro, executei o Aristóteles por @HarmonicMath, que em cerca de 15 horas formalizou completamente a prova. Depois, com a grande ajuda de @PietroMonticone, consegui configurar uma versão de esboço da prova. Esta é uma versão na qual 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 fase de pós-processamento, também usei o Grok Heavy e o Codex CLI com o GPT-5.2 no modo xhigh para escrever uma análise linha por linha da prova formal. Isso é uma grande ajuda para pessoas que não são programadores profissionais de Lean 4. Você pode realmente internalizar todos os passos 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