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

Artigos matemáticos precisam de validação formal. Isso geralmente é feito informalmente por um árbitro. Mas e se pudéssemos confiar em algo mais robusto, como a autoformalização para Lean 4, onde o papel do árbitro seria reduzido a uma verificação meticulosa das formulações das definições e teoremas? A compilação de código gerado automaticamente se tornaria um certificado de prova. Isso foi o que aconteceu em uma série mais longa, que fiz com Aristóteles de @HarmonicMath. Obrigado à @PietroMonticone e à @llllvvuu pela ajuda na configuração do blueprint. Aqui apresento uma autoformalização completa e correta de um artigo do meu amigo Stefan Barańczuk sobre sequências de divisibilidade de Chebyshev. O código tem cerca de 5000 linhas de lean altamente não trivial. Corrige todas as inconsistências e lacunas no artigo principal (até provando algumas proposições delegadas). Vou postar uma série desses experimentos, provando que em algumas áreas da matemática, incluindo teoria elementar dos números, combinatória e análise (todos os tipos de coisas abordadas pelo Mathlib), não estamos longe de uma mudança massiva na documentação da validade das provas. Acho que este vai ser um ano agitado!

Se eu fosse estudante hoje, interagir com LLMs de última geração pareceria quase como colar. Esta manhã, tirei aleatoriamente uma foto do quadro negro e pedi ao ChatGPT-5.2-Pro que explicasse o contexto, a solução e algumas observações paralelas sobre o famoso teorema de Chevalley sobre conjuntos construtíveis. O que recebi foi um relatório notavelmente profundo, sintetizando material de alta qualidade sobre geometria algébrica retirado de toda a internet. Isso levanta uma questão séria: qual é o verdadeiro esforço e desafio para os estudantes hoje? O custo certamente é um fator, mas uma vez que o acesso a esses modelos esteja disponível, como alguém deve aprender nesta terra de abundância, onde explicações, referências e exploração interativa são instantaneamente acessíveis? Talvez a luta não seja mais sobre obter informações ou mesmo entender argumentos individuais, mas sim desenvolver julgamento: saber quais perguntas fazer, quais explicações confiar, como reconhecer a profundidade versus a plausibilidade superficial, e como internalizar ideias em vez de apenas consumi-las. Em um ambiente onde as respostas são abundantes, a verdadeira dificuldade pode estar em formar gosto, intuição matemática e a capacidade de navegar — em vez de se afogar — nesse súbito excesso de conhecimento.