Um companion em Lean para Analysis I
(terrytao.wordpress.com)- Terence Tao iniciou um repositório companion que transfere para código Lean as definições, teoremas e exercícios do livro-texto de análise real Analysis I
- Como o livro trata de forma rigorosa a construção dos números naturais, inteiros, racionais e reais, além de teoria dos conjuntos e lógica, ele tem uma estrutura adequada para estudar com um assistente de provas
- O escopo atual cobre parte do capítulo 2, teoria básica dos conjuntos na seção 3.1 e inteiros até a seção 4.1, incluindo também um isomorfismo com os números naturais da Mathlib
- O código compila em Lean, mas ainda restam muitos
sorry, e a recomendação é preenchê-los em forks em vez de publicar soluções oficiais - O material pode ser usado tanto como um caminho alternativo para resolver exercícios em Lean quanto como uma introdução ao uso da Mathlib, especialmente nos capítulos mais avançados
Projeto para converter Analysis I para Lean
- Lean companion to “Analysis I” é um projeto para “traduzir” para Lean várias definições, teoremas e exercícios de Analysis I
- Os exercícios do livro também podem ser resolvidos preenchendo os
sorrycorrespondentes no código Lean - Não há planos de hospedar soluções oficiais dos exercícios no companion; versões com os
sorrypreenchidos podem ser criadas como forks do repositório
Por que o livro e Lean combinam bem
- Analysis I é um livro que se concentra mais em questões fundamentais para complementar livros-texto tradicionais de análise real
- Construção dos números naturais, inteiros, racionais e reais
- Teoria dos conjuntos e lógica para permitir o desenvolvimento de provas com alto rigor
- Quando o livro foi escrito, assistentes de provas como Coq e Agda já existiam, mas verificação formal não era uma área de interesse na época
- Depois de experiências com verificação formal, ficou claro que o conteúdo do livro combina bem com assistentes de provas
- A teoria ingênua de tipos usada implicitamente no livro ao construir os sistemas numéricos padrão se alinha bem à teoria de tipos dependentes de Lean
- O suporte de Lean a quotient type também se encaixa no método de construção usado no livro
Escopo atualmente convertido para Lean
- Atualmente, as seguintes seções foram traduzidas para Lean
Relação com a Mathlib
- A formalização foi projetada para, em alguns pontos, ficar separada da biblioteca matemática padrão de Lean, a Mathlib, e, em outros, depender dela
- A Mathlib já tem uma noção padrão de números naturais
- Na formalização em Lean, primeiro é desenvolvida uma
Chapter2.Nat, que reconstrói os números naturais “à mão”- Ao trabalhar no namespace
Chapter2, ela pode ser usada comoNat - São estabelecidos resultados básicos paralelos aos lemas auxiliares sobre números naturais da Mathlib
- Muitas dessas provas foram deixadas como exercícios para o leitor e atualmente são substituídas por
sorry
- Ao trabalhar no namespace
- A seção de epílogo estabelece um isomorfismo entre esses números naturais alternativos e os números naturais da Mathlib
- Mais precisamente, esse isomorfismo também é formulado como exercício
- Depois disso, a construção de números naturais do capítulo 2 deixa de ser usada, e passam a ser usados os números naturais da Mathlib
- A ideia é seguir, nos capítulos posteriores do livro, um padrão de depender cada vez mais de definições e funções da Mathlib em vez das construções próprias dos capítulos iniciais
Modo de uso e estado da verificação
- O código do repositório compila em Lean
- Porém, ainda não foi testado se todos os muitos
sorryno código podem de fato ser preenchidos - Também é necessário verificar se os lemas auxiliares necessários e a API dos arquivos Lean são suficientes
- O objetivo é confirmar se é possível preencher os
sorryde maneira conceitualmente natural, sem depender de técnicas obscuras de programação em Lean
- O objetivo é confirmar se é possível preencher os
- O autor gostaria que voluntários fizessem playtest do companion para verificar se os exercícios podem de fato ser resolvidos em Lean
- Outros feedbacks também são bem-vindos
Como material introdutório a Lean e Mathlib
- Este companion pode ser usado não só para análise real, mas também como introdução a Lean e Mathlib
- Nesse aspecto, ele é um pouco parecido com o Natural number game
- O Natural number game tem grande sobreposição temática com o capítulo 2 de Analysis I
1 comentários
Comentários do Hacker News
Acho que o ponto mais interessante ao ensinar matemática com Lean é o feedback imediato. Se a prova do aluno estiver errada, ela simplesmente não compila
Antes, só era possível receber feedback se alguém como um monitor, instrutor ou especialista revisasse; agora, o compilador do Lean pode dar feedback rapidamente
No futuro, seria bom se o compilador do Lean também oferecesse feedback mais educativo, assim como o compilador do Rust sugere correções de código, e talvez isso exija um LLM dedicado
Antigamente, estudar matemática envolvia muito tempo ruminando uma tarefa, testando coisas no papel, e esse processo às vezes levava à internalização de conceitos e a novas ideias
Com Lean, talvez isso vire um modo de simplesmente tentar, checar aleatoriamente e despejar tentativas. Quando mexi algumas vezes com Coq, também ficou a lembrança de ter passado a maior parte do tempo cutucando e tentando coisas
reduce(r.num, r.denom) = reduce(a, b)cross_equals(a, b, r.num, r.denom)r.denom * a = r.num * bEle não usa LLM; há um pequeno modelo local rodando dentro da extensão do VS Code. Tomara que um dia esse pequeno modelo local fique forte o bastante para superar em muito os humanos. Há mais detalhes em https://acornprover.org/docs/tutorial/proving-a-theorem/
Estou realmente animado. Seria ótimo se isso fosse movido para um repositório separado, para ficar mais fácil de encontrar e enviar a outras pessoas
Eu já tinha curiosidade por matemática, e o Analysis do Tao foi o primeiro livro que me mostrou como a matemática é construída de um jeito rigoroso que minha cabeça de programador esperava
Depois também brinquei um pouco com Lean e tive uma satisfação parecida, mas a Mathlib era bem complexa para aprender conceitos matemáticos. Por isso fico feliz com a criação de uma ponte entre o livro e a ferramenta
É bom ver a prova de teoremas ganhando tração em temas matemáticos mainstream como análise
Na área de teoria de linguagens de programação, quando as ferramentas já tinham começado a ficar bem polidas em meados da década de 2010, um livro-texto de referência como The Formal Semantics of Programming Languages, de Winskel, chegou a ser formalmente verificado em Isabelle. Não é uma transcrição 1:1 completa, mas http://concrete-semantics.org é esse exemplo
Se você tem interesse em prova de teoremas, pessoalmente acho que esse lado é um ponto de partida muito mais fácil. Afinal, os teoremas de análise já são, por si só, bastante difíceis
Você faz indução estrutural, aplica a hipótese de indução para mostrar que o invariante é preservado e segue em frente
Não é que eu tenha feito muitas provas de teoremas nem provas “matemáticas” como análise em assistentes de prova, mas, se provas matemáticas exigem uma abordagem muito diferente, fico curioso sobre quanta transferência de habilidade existe entre as duas
Também quero mencionar o Software Foundations, do Rocq. Talvez exista um porte para Lean, mas, quando acompanhei a parte inicial, foi bastante agradável
Seria muito interessante avaliar como a abordagem mainstream de “livro-texto” difere da abordagem da Mathlib
Em geral, bibliotecas de matemática formalizada enunciam resultados da forma mais geral possível e facilitam refatorar o desenvolvimento das provas para algo mais intuitivo e elegante
A refatoração é fácil porque o sistema sempre rastreia o que decorre logicamente do quê. Ao trabalhar com papel e caneta, isso não existe, então muitas oportunidades de retrabalho acabam passando despercebidas
Uma pergunta natural é se faz sentido ensinar análise real na graduação na versão de “máxima generalidade” ao estilo da Mathlib. Claro, o mesmo vale para outras áreas da matemática baseada em provas
Pelo que sei, a experiência de professores que tentaram isso de fato foi parecida. Para alunos mais avançados pode ser bom, mas, para o aluno médio, há grande chance de desperdiçar tempo de aula
Meu viés vem do fato de eu ter aprendido conceitos matemáticos por artigos
Sinto que código impõe uma carga adicional enorme e, em geral, muitas vezes não segue nenhum critério de estilo. Falando como alguém que já teve que ler artigos de matemática considerados incompreensíveis, código é 10 vezes pior, porque praticamente não há critério algum de compreensibilidade
No canal do próprio Terence Tao no YouTube também há alguns vídeos em que ele usa Lean. https://www.youtube.com/@TerenceTao27
Não sei os detalhes, mas foi legal vê-lo trabalhando com e sem LLM
Para um tema fundamental como análise, acho que é um projeto muito bom e uma boa abordagem
As duas preocupações que me vêm imediatamente à cabeça são estas. Primeiro, os resultados centrais de análise da Mathlib usam o conceito de filtros para tratar limites de forma geral e unificada. Ainda assim, alguns resultados são especializados em forma epsilon-delta. Imagino que o Analysis do Tao use uma abordagem epsilon-delta mais tradicional
Segundo, a Mathlib se move rápido e quebra com frequência. Nomes mudam e refatorações continuam acontecendo, então repositórios dependentes exigem manutenção contínua
https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6
É uma ideia bem radical, mas acho que a educação matemática deveria se concentrar em criar sistemas de álgebra computacional, como o Mathematica, e provadores de teoremas, como o Lean. Visualização e aplicações práticas também deveriam entrar com força.
No extremo, poderia ser um formato em que a pessoa não faz matemática no papel de forma alguma, mas consegue provar dentro do Lean tudo o que aprendeu.
O sistema atual se concentra em cálculos manuais intermináveis, e sinto que isso parece inútil demais e tedioso, fazendo as pessoas odiarem matemática.
Material didático de Lean, que bom. Mas por que não há HoTT?
“Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
https://news.ycombinator.com/item?id=43196452
Mais materiais sobre Lean que apareceram no HN esta semana:
“100 theorems in Lean”
https://news.ycombinator.com/item?id=44075061
“Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725
Não sei a motivação exata, pois está fora da minha área, mas parece que Agda é uma maneira melhor do que Lean para formalizar essas ideias.
Até o fim deste ano também deve sair um novo material didático que é uma atualização mais moderna do livro existente de HoTT, e há também uma formalização em Agda.
https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
https://github.com/HoTT-Intro/Agda
HoTT não está nem perto de ser aceita como um padrão razoável e, para a maioria das pessoas, é um assunto que já trava logo no começo.
É parecido com perguntar a um desenvolvedor de frameworks JavaScript por que ele não fez um framework para Elm ou Haskell.
Foi investido muito menos trabalho em tornar provadores de teoremas HoTT fáceis de usar, e a documentação também é muito mais pobre.
As vantagens da HoTT também não são claras. Parece que ela só reduz o trabalho ao lidar com construções extremamente obscuras da teoria das categorias.
Terrence Tao tem alguns livros de análise, e este é um material complementar em Lean para o primeiro deles. Ele não tem um livro de teoria dos tipos, então não há teoria dos tipos de ordem superior. A proposta, para começo de conversa, é totalmente diferente.
Muito legal. Analysis I foi o primeiro livro de matemática “de verdade” que eu, sendo engenheiro e não matemático, senti que conseguia acompanhar e resolver completamente, depois de tentar várias vezes outros livros como Rudin.
Espero que o material complementar em Lean o torne mais acessível para pessoas familiarizadas com matemática e programação que queiram aprender com rigor.
Nos últimos anos, houve tentativas constantes de formalizar em Lean o livro Analysis I de Tao, e houve pessoas tentando fazer exatamente o mesmo que Tao está fazendo agora. Infelizmente, a maioria não passou dos primeiros capítulos, mas espero que Tao consiga ir mais longe
Eu mesmo cheguei a pensar em tentar. Achei que anexar provas formalizadas de cada exercício ao meu blog de comentários sobre Analysis I, https://taoanalysis.wordpress.com/, seria útil para quem estivesse acompanhando o livro
Também postei no servidor Discord privado do livro, mas compartilho aqui estes materiais relacionados porque parecem poder ajudar
https://github.com/cruhland/lean4-analysis — derivado de https://github.com/cruhland/lean4-axiomatic
https://github.com/Shaunticlair/tao-analysis-lean-practice
https://github.com/vltanh/lean4-analysis-tao
https://github.com/gabriel128/analysis_in_lean
https://github.com/mk12/analysis-i
https://github.com/melembroucarlitos/Tao_Analysis-LEAN
https://github.com/leanprover-community/NNG4/ — não segue o livro de Tao, mas é a versão em Lean4 do jogo dos números naturais, então o conteúdo é muito parecido com o do capítulo 2
https://github.com/djvelleman/STG4/ — é um jogo de teoria dos conjuntos em Lean4, então pode ser parecido com o capítulo 3. Porém, em https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean aparece
import Mathlib.Data.Set.Basic, então parece importar os conjuntos do Lean em vez de redefinir conjuntos do zero e estabelecer axiomas. Essa abordagem pode fazer com que o Lean “saiba demais” sobre teoria dos conjuntos, o que talvez não seja bom para o objetivohttps://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — para a construção dos inteiros
https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — pode ser o mesmo arquivo acima
https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — para a construção dos racionais
https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — mostra uma forma de definir um tipo
Setpersonalizado