O companion em Lean de Analysis I

• Projeto que transpõe os pontos centrais de Analysis I, o livro-texto de análise real escrito por Terence Tao, para o assistente de provas Lean
• O projeto tem uma estrutura que combina bem com os objetivos do livro original, que enfatiza a construção dos sistemas numéricos básicos e a lógica das demonstrações
• Usa a biblioteca padrão Mathlib, mas inclui também a construção direta dos principais conceitos e exercícios em que os leitores fazem as provas por conta própria
• É possível praticar preenchendo diretamente os espaços em branco (sorry) no código Lean, sem solução oficial, com possibilidade de expandir o trabalho por meio de um fork
• É útil tanto para iniciantes em Lean quanto para estudantes de análise real, por oferecer uma chance de experimentar o uso prático de Mathlib e Lean

---

Visão geral

• Projeto open source que reconstrói em Lean, ferramenta assistente de provas, o livro-texto de análise real "Analysis I", escrito por Terence Tao
• Em comparação com outros livros de análise, esta obra dá mais foco ao processo de construção dos números naturais, inteiros, racionais e reais, bem como às ferramentas de teoria dos conjuntos e lógica necessárias nesse processo
• Grande parte do livro se concentra no desenvolvimento da capacidade de fazer demonstrações rigorosas de forma sistemática, o que combina muito bem com um assistente de provas como o Lean

Características do projeto companion em Lean

• Fornece uma "tradução" para o formato Lean das definições, teoremas e exercícios do livro original
• Esses arquivos Lean incluem muitos espaços em branco (sorry) correspondentes às soluções dos exercícios, permitindo que o leitor aprenda preenchendo-os por conta própria
• Não há explicações oficiais (soluções), mas o leitor pode fazer um fork do repositório e criar sua própria versão com respostas

Integração com Mathlib e diferenças

• Alguns conceitos já implementados na Mathlib (a biblioteca matemática padrão do Lean), como os números naturais, são propositalmente reconstruídos separadamente, e depois o projeto propõe provar a isomorfia (equivalência) com a versão da Mathlib
• Como exemplo, em Chapter2.Nat, o projeto constrói do zero uma definição própria de números naturais, distinta da usada pela Mathlib, trata diretamente os principais resultados e, ao final, propõe que o usuário pratique em Lean mostrando que as duas versões são equivalentes
• A partir dos capítulos seguintes, o fluxo passa a aproveitar gradualmente mais as definições e funcionalidades da Mathlib

Como aprender e usar

• Este companion em Lean serve não só para o estudo de análise, mas também como introdução à forma de formalizar matemática em Lean e Mathlib
• Assim como no "Natural number game", ele inclui exercícios estruturados em que se pode definir e praticar diretamente objetos matemáticos dentro do ambiente Lean
• O código em si pode ser compilado em Lean, mas ainda não houve verificação completa de que todos os exercícios (sorry) são de fato solucionáveis, de modo que playtesting e feedback ainda são necessários

Open source e contribuições

• O repositório é open source e qualquer pessoa pode consultá-lo, fazer fork e contribuir
• Não são fornecidas soluções oficiais em separado, e o projeto permite a criação de múltiplas versões de resolução
• Em 31 de maio, o projeto foi movido para um repositório independente separado

[GN⁺]

Comentários do Hacker News

• Estou realmente animado com isso; se este projeto for movido para um repositório independente, será bem mais fácil para outras pessoas compartilharem e encontrarem. Sempre tive curiosidade sobre matemática, e o Analysis do Tao foi o primeiro livro didático que me mostrou como a matemática é construída de forma rigorosa de um jeito que combinava com minha forma de pensar em programação. Depois, também acabei me interessando por Lean, mas achei o Mathlib um pouco complicado para aprender conceitos matemáticos. Então gosto muito deste projeto por servir como uma ponte entre o livro e a ferramenta.

  • Tive uma experiência parecida. Aprendi sobre convergência, sequências de Cauchy etc., e lembro que este livro foi publicado pela Hindustan Book Agency, uma editora sem fins lucrativos da Índia, então era muito barato de conseguir.

• O aspecto mais empolgante da educação matemática com Lean, para mim, é o feedback imediato. Se o aluno errar a prova, ela não compila. Antes, era preciso que uma pessoa — um TA ou professor — desse esse feedback diretamente, mas agora o compilador do Lean avisa rápido. Espero que no futuro apareça algo como o compilador do Rust, oferecendo até sugestões amistosas de correção (isso talvez exija um LLM dedicado).

  • Também concordo em quase tudo, mas acho que o processo de quebrar a cabeça com a prova também é importante. Minha experiência com matemática já faz tempo, mas havia muito daquele tempo de "paraíso matemático" de escrever tarefas ou problemas no papel e pensar com calma. Com Lean, me preocupo que isso possa virar mais um processo de ficar digitando coisas aleatoriamente ou tentando até acertar automaticamente, mais centrado no manuseio da ferramenta. Cheguei a usar coq um pouco no passado, e lembro que era quase só mexer e testar o tempo todo. Em resumo, theorem solvers são úteis em muitos aspectos, mas fico pensando se esse processo lento de absorção, internalização, conceitualização e surgimento de novas ideias pode acabar se enfraquecendo. Gostaria de saber o que vocês acham disso.

• Há um canal pessoal no YouTube onde dá para ver o próprio Terence Tao usando Lean. Não sou especialista na área, mas achei fascinante só de ver como ele trabalha com ou sem LLM (https://www.youtube.com/@TerenceTao27).

• Acho que seria muito interessante avaliar e comparar a abordagem tradicional de "livro didático" com o estilo do Mathlib. Bibliotecas de matemática formalizada geralmente têm a vantagem de expressar resultados da forma mais geral possível, e também é fácil refatorar a própria estrutura das provas para deixá-las elegantes. Refatorar é fácil porque o sistema sempre rastreia as dependências lógicas, mas isso não é simples quando se trabalha só com papel e caneta. Então parece natural se perguntar se seria adequado ensinar, em disciplinas universitárias, uma análise na versão de "máxima generalidade" como a do Mathlib. Acho que essa mesma questão vale para todas as áreas da matemática baseadas em provas.

  • Pelo menos em cursos introdutórios, acho que não é adequado. Já há coisa demais para entrar no currículo — métodos de prova, programação e teoria básica. A experiência de professores que realmente tentaram isso também parece semelhante: para alunos avançados é bom, mas para os alunos em geral costuma ser perda de tempo.

  • Como matemático que também programa há muito tempo, penso que nenhuma formalização programática vai desenvolver entendimento fundamental. Meu viés vem do fato de eu ter aprendido conceitos por meio de artigos. Código costuma ser avassalador em termos de legibilidade porque muitas vezes não se preocupa com estilo; artigos ilegíveis já são difíceis, mas com código é 10 vezes pior na minha experiência, porque nem existe um padrão.

• Fico feliz em ver theorem proving ganhando cada vez mais atenção em áreas mais centrais da matemática, como análise. Em PLT, já houve o caso representativo de The Formal Semantics of Programming Languages, do Winskel, formalmente verificado em Isabelle (http://concrete-semantics.org). Se alguém quiser começar com theorem proving, acho que aquele lado é mais fácil e mais recomendável. Também vale acrescentar que os teoremas em análise já são bastante difíceis por natureza.

  • Eu também não ficaria surpreso se provas em PL tiverem uma barreira de entrada menor. Também ouço muito que elas têm um ar mais rotineiro — indução estrutural, aplicar indução, provar invariantes, repetir esse fluxo. Não fiz muito theorem proving, mas nunca tentei fazer provas matemáticas (especialmente de análise) em um theorem prover. Tenho curiosidade sobre se provas "matemáticas" exigem uma abordagem muito diferente e até que ponto há transferência de habilidade entre as duas coisas. Como referência, estudei Software Foundations em Rocq (talvez exista uma versão portada para Lean?) e foi bastante divertido.

• Acho que este projeto e esta abordagem combinam muito bem com temas básicos como análise. Mas tenho duas preocupações

  1. Os resultados centrais de análise no Mathlib são tratados de forma unificada com o conceito de filtro (filter), e em casos especiais separadamente no estilo epsilon-delta. Imagino que o Analysis do Tao use uma abordagem mais tradicional de epsilon-delta.
  2. O Mathlib é um projeto que muda rápido, então nomes e estruturas estão sempre mudando. A informação de integração teria de ser mantida continuamente.
  • Para quem quiser conferir por conta própria, a maior parte do capítulo sobre o limite de sequências está disponível como páginas de amostra, então vale ver o link relacionado: https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6

• Acho um projeto muito legal. Analysis I foi o primeiro livro didático de matemática "de verdade" que eu, como engenheiro, consegui realmente estudar até o fim acompanhando tudo, e já tinha falhado várias vezes tentando com outros livros (como Rudin). Se existir uma versão em Lean, acho que pessoas familiarizadas tanto com matemática quanto com programação poderão aprender os conceitos com mais rigor.

• Ao longo dos anos, houve várias tentativas de fazer uma formalização oficial em Lean do Analysis I do Tao, mas sempre foi difícil avançar além de alguns capítulos. Por um tempo eu mesmo quis tentar isso — achei que seria útil para quem estuda com o livro publicar junto provas formalizadas conectadas ao blog de soluções do Analysis I (https://taoanalysis.wordpress.com/). Já compartilhei, em um Discord privado, o que estava organizado, mas vou reunir aqui vários projetos de referência em Lean que podem ser úteis para muita gente (github, gist, documentação oficial etc.).

  • https://github.com/cruhland/lean4-analysis
  • 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/ (isto não é o livro do Tao, mas sim a versão Lean4 do jogo dos números naturais, com conteúdo quase idêntico ao do Capítulo 2)
  • https://github.com/djvelleman/STG4/ (da mesma forma, o jogo de teoria dos conjuntos, parecido com o Capítulo 3; mas, olhando para Game/Metadata.lean, ele faz import Mathlib.Data.Set.Basic e não redefine teoria dos conjuntos do zero — nesse caso, o Lean já "sabe" toda a teoria dos conjuntos, então talvez isso não seja perfeito para nosso objetivo)
  • https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc (exemplo de 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 (exemplo de construção dos racionais)
  • https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality (exemplo de referência para definir um tipo Set customizado)

• Tenho curiosidade sobre quão importante realmente é a "prova de isomorfismo com o objeto correspondente no Mathlib". Será que, se você deixar essa parte de fora, na prática nada muda? Por exemplo, isso é usado de verdade para coisas como traduzir teoremas automaticamente?

  • Esse tipo de prova de isomorfismo

    1. Permite provar que o objeto que você construiu e o objeto já existente no Mathlib são de fato o mesmo, especialmente porque, no lado do Mathlib, ele pode estar definido por uma construção generalizada e complexa, o que ajuda a entender a diferença.
    2. Tem um papel decisivo para entender a notação e a terminologia oficiais usadas no Mathlib para ler ou escrever esse objeto.

  • Acho que pelo menos há valor educacional. Isso vira um processo em que a própria pessoa se convence de que o conjunto e as operações que construiu são "os mesmos" em outras partes do livro também.

• Fico feliz em ver o surgimento de livros didáticos baseados em Lean. Mas por que não há HoTT (Homotopy Type Theory)? Existe até um post com a pergunta "Type Theory (HoTT) should replace (ZFC) set theory?" (https://news.ycombinator.com/item?id=43196452). Também compartilho recursos adicionais da comunidade sobre Lean que apareceram no HN esta semana — "100 theorems in Lean" (https://news.ycombinator.com/item?id=44075061) e o projeto Lean da DeepMind (https://news.ycombinator.com/item?id=44119725).

  • Mas também não vejo por que precisaríamos chegar até HoTT. Theorem provers de HoTT ainda têm pouca usabilidade, e a documentação também não é suficiente. Também não sinto que os ganhos trazidos por HoTT sejam claros; normalmente parece relevante só ao lidar com estruturas extremamente peculiares, como em teoria das categorias.

  • Como a abordagem é a de um livro didático tradicional, a pergunta "por que não HoTT?" já vem respondida por si só. Além disso, acho que há muitos especialistas céticos quanto ao efeito educacional.