Lean4 ajuda a encontrar um pequeno bug em artigo recente de Terence Tao

• Post de Terence Tao no mathstodon.xyz
• Um bug pequeno, mas importante, foi encontrado em um artigo recente de Terence Tao devido ao projeto de formalização em Lean4
• O bug foi descoberto durante o processo de formalização na página 6 do artigo, que pode ser consultado em https://arxiv.org/pdf/2310.05328.pdf
• No artigo de Tao, foi encontrada a expressão divergente 12log⁡n−1n−k−1 no caso n=3, k=2
• O problema existe apenas para valores pequenos de n e pode ser resolvido alterando algumas constantes numéricas na página
• Para n≥8, a lógica continua válida, e os casos de n pequeno podem ser tratados por um método mais simples
• Lean4 pediu a Tao que provasse 0<n−3, mas ele tinha apenas a hipótese n>2, o que revelou a inconsistência
• Tao planeja adicionar uma nota de rodapé em uma nova versão do artigo reconhecendo o pequeno erro encontrado após tentar a formalização em Lean4
• Este post despertou interesse e reações positivas da comunidade, destacando a importância dos assistentes de prova para estabelecer uma base sólida para trabalhos futuros

[GN⁺]

Comentários do Hacker News

• O renomado matemático Terence Tao usou Lean4 e GPT4 para encontrar um pequeno bug em um artigo recente.
• O processo de aprendizado de Tao com Lean4 foi registrado em suas postagens no Mastodon, tornando-se um estudo de caso interessante sobre como o Lean4 pode acelerar o trabalho.
• Para iniciantes, o Natural Number Game é recomendado como uma introdução fácil ao Lean4.
• Um usuário compartilhou sua experiência usando o TLA+ de Lamport para gerar especificações formais e reduzir erros na programação.
• Há interesse em tipos dependentes, apesar da complexidade de implementá-los em compiladores.
• A combinação de Lean4 com prova automática parece ser uma combinação tecnológica promissora para o futuro, com potencial para impulsionar novas descobertas.
• O fato de Tao estar aprendendo Lean com o Copilot foi destacado como um exemplo de como o Lean4 pode reduzir a fricção na adoção de novas ferramentas.
• O progresso de Tao com Lean4 pode ser acompanhado em seu GitHub.
• Um usuário propôs a ideia de combinar verificadores formais de provas com modelos de linguagem para gerar pares sintéticos de conjectura-prova, o que pode evoluir para capacidades sobre-humanas na geração de provas.
• O termo "bug" foi usado para descrever um erro matemático, o que alguns usuários acharam incomum.