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!