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!