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

Os artigos matemáticos precisam de validação formal. Isso é geralmente feito informalmente por um árbitro. Mas e se pudéssemos contar com algo mais robusto, como a auto-formalização em 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 do código gerado automaticamente se tornaria um certificado de prova. Isso foi o que aconteceu em um projeto mais longo que fiz com Aristóteles por @HarmonicMath. Agradeço a @PietroMonticone e @llllvvuu por ajudarem na configuração do projeto. Aqui apresento uma auto-formalizaçã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. Ele corrige todas as inconsistências e lacunas no artigo principal (até provando algumas proposições delegadas). Vou postar uma série de tais experimentos, provando que em algumas áreas da matemática, incluindo teoria dos números elementar, combinatória e análise (todos os tipos de coisas cobertas 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 um estudante hoje, interagir com LLMs de última geração pareceria quase uma trapaça. Esta manhã, tirei aleatoriamente uma foto do quadro e pedi ao ChatGPT-5.2-Pro para explicar o contexto, a solução e algumas observações 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 está disponível, como deve um aprender nesta terra de abundância, onde explicações, referências e exploração interativa estão todas instantaneamente acessíveis? Talvez a luta não seja mais sobre obter informações ou mesmo entender argumentos individuais, mas sobre desenvolver julgamento: saber quais perguntas fazer, quais explicações confiar, como reconhecer profundidade versus 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 - neste súbito excesso de conhecimento.