A matemática está assombrada

• Lean é uma linguagem de programação projetada para formalizar a matemática, permitindo que matemáticos tratem teoremas matemáticos como código
• Usuários escrevem teoremas, provas, axiomas etc. em formato de código, e o processo da prova é conduzido por meio de um conjunto de comandos chamado tactic
• Mesmo que a prova não esteja realmente completa, é possível encerrá-la provisoriamente com sorry; isso funciona como uma prova falsa, semelhante ao any do TypeScript
• Se forem adicionados axiomas incorretos (por exemplo, 2 = 3), surge o risco de inconsistência lógica e da possibilidade de provar qualquer afirmação
• Como Lean extrai conclusões apenas a partir dos axiomas escolhidos e do sistema de prova lógico, manter a validade matemática tem grande importância

---

Lean: linguagem para lidar com matemática como código

• Lean é uma linguagem de programação especializada em escrever matemática formalizada
• Matemáticos podem, por meio de Lean, expressar matemática como código e estruturar seus teoremas e provas para viabilizar colaboração e compartilhamento
• O texto também sugere um futuro em que uma grande parcela do conhecimento matemático humano poderá ser representada em código, passível de verificação e composição mecânicas

O primeiro passo das provas em Lean

• Em Lean, é possível declarar um teorema simples no formato theorem two_eq_two : 2 = 2 := by sorry
• Quando a prova está incompleta, coloca-se sorry, mas isso é apenas uma solução temporária, não uma prova real
  • sorry passa pela verificação de prova do Lean, mas não é confiável do ponto de vista lógico
• Para uma prova completa, usa-se uma tactic como rfl (reflexividade) para provar identidades óbvias como 2 = 2
• O que já foi provado pode ser reutilizado em outro teoremas com exact e similares, destacando a modularidade

Axiomas e contradições: quando a matemática está assombrada

• Se adicionarmos um axioma como axiom math_is_haunted : 2 = 3, Lean o trata como verdadeiro
• Esse axioma pode ser usado nos passos seguintes da prova, tornando possível provar conclusões matematicamente absurdas, como 2 + 2 = 6
• É possível substituir 2 por 3 usando a tactic rewrite e encerrar o raciocínio da igualdade com rfl
• Se uma contradição for induzida por axiomas inadequados, também no Lean ocorre um estado em que qualquer proposição pode ser provada (colapso lógico)
• Na prática, no início do século XX, inconsistências em sistemas axiomáticos, como o paradoxo de Russell, levaram a reflexões fundamentais sobre a matemática
• Assim, Lean mostra bem que a escolha de axiomas é decisiva para a manutenção da validade de um sistema lógico

Lean como verificador de provas

• Se os axiomas forem bem selecionados e Lean for logicamente correto, ele oferece conclusões com confiabilidade teórica
• Desde equações simples até teoremas muito complexos (como o Teorema de Fermat) são verificados pelo mesmo princípio
• Um grande teorema é construído como uma árvore inteira por meio da acumulação repetida de provas de subestruturas e teoremas menores
• Como exemplo, há um projeto de grande escala em andamento para formalizar o Teorema de Fermat em Lean, e espera-se que no fim seja concluída uma prova formal sem sorry provisórios

A diversão de aprender Lean

• Provar com Lean é uma combinação criativa de programação e matemática
• Começa-se aprendendo a provar proposições simples, e gradualmente se torna a principal diversão construir matemática cada vez mais complexa e profunda de forma rigorosa
• Manuais oficiais e materiais da comunidade (como Natural Numbers Game, Mathematics in Lean etc.) são adequados para iniciantes
• Ao usar Lean, você pode formalizar diretamente a lógica e redescobrir a beleza de ideias e argumentos engenhosos
• Sem motivo aparente, a conclusão é que Lean oferece uma diversão especial para certos tipos de pessoas

[GN⁺]

Comentários no Hacker News

• Ando pensando na ideia de reescrever notícias ou artigos de não ficção usando sistemas parecidos com o Lean (ou o próprio Lean), tratando cada afirmação como um teorema que precisa ser provado, com a prova incluindo citações; por exemplo, daria para tratar algo como “se três fontes que eu aprovei afirmam isso como fato, então isto é um fato” como uma prova composta, e acho que seria possível marcar o documento inteiro para destacar as afirmações “provadas”; não seria perfeito, mas seria uma tentativa de recriar com tecnologia o rigor que o jornalismo costumava oferecer
  • Formalizar afirmações em linguagem natural é uma área cheia de dificuldades, por razões parecidas com as de escrever código que interage com o mundo real; todos os conceitos que tomamos como óbvios (identidade, tempo, causalidade etc.) precisam ser tratados com muito detalhe dentro do formalismo para que os fatos possam ser conectados ou até expressos; ainda assim, o problema é realmente fascinante; o OpenCog foi um projeto que levou isso até o limite, e também existe na academia uma área específica chamada representação de conhecimento e raciocínio (KRR); o periódico IJCAI também está cheio de pesquisas relacionadas, e há muitas lógicas criadas por filósofos para formalizar diferentes tipos de argumentação, como tempo/modalidade/probabilidade, mas infelizmente elas não se combinam facilmente entre si (a menos que isso tenha sido resolvido recentemente)
  • Acho que a crença mais importante que devemos ter sobre notícias geralmente não é algo que possa ser provado como um conjunto de afirmações absolutas; ferramentas que calculam cadeias de inferência, como probabilidade bayesiana, me parecem mais adequadas; já vi ferramentas para fazer estimativas numéricas nesse estilo
  • Tive a experiência de melhorar muito minha escrita de não ficção depois de estudar matemática na universidade; ao ler ensaios escritos pela minha SO (companheira) e pela minha irmã mais nova, eu aplicava um rigor quase de prova lógica, tipo: “aqui você diz que C vem de B, mas falta justamente por que B vem de A, então não dá para dizer que C vem de A”; parece plausível transformar isso em programa com ferramentas como LLM, mas as alucinações (geração de afirmações que não existem nos fatos) tornam os limites bem claros
  • É preciso ter cuidado; esse tipo de abordagem pode facilmente dar uma aura de objetividade lógica a afirmações que, no fundo, sejam radicais demais ou simplesmente sem sentido; as posições políticas de Gottlob Frege, um dos pais da lógica moderna, podem servir de alerta link relacionado
  • Acho que seria mais interessante um jeito de desenhar como mapa toda a estrutura de argumentação sobre um tema específico; por exemplo, começar com uma grande pergunta como “Deus existe?”, e então abrir hierarquicamente todos os argumentos a favor, contra, as objeções e as contra-objeções; em cada afirmação, citações do tipo “Platão fez esse argumento” entrariam mais para dar contexto histórico do que como evidência; o ponto principal não é decidir o vencedor, mas criar um mapa de argumentos para não ficar girando em torno dos mesmos pontos
• Fico me perguntando se no fim estamos criando um dicionário de provas que parte de algumas verdades autoevidentes, e em cima dele várias provas vão sendo empilhadas logicamente; aí provas adicionais seriam só combinações lógicas de provas já existentes; queria muito que transformassem isso num jogo estilo Zachtronics! Um jogo chamado Euclidea passa um pouco essa sensação no campo da trigonometria, e a ideia de ir construindo essa torre de lógica é fascinante demais; será que matemática pura é justamente isso, e será que professores de matemática pura sentem prazer em expandir esse dicionário lógico? E lembro de algum matemático famoso que fez uma lista de provas básicas; se alguém souber quem/o quê era e como isso se chamava, seria ótimo; imagino que sejam os axiomas
  • Já existe um jogo relacionado, embora talvez não seja exatamente o que você quer (e também não é um jogo de construir toda a matemática); joguei e achei bem divertido; o exemplo é justamente leanprover-community/nng4, mencionado no artigo
  • Sobre “façam disso um jogo estilo Zachtronics”, dá para dizer que matemática é esse jogo (meio brincando, mas nem tanto); também acho que uma versão gamificada seria realmente divertida; matemática pura é justamente esse tipo de sistema; na graduação essa sensação bate bem, embora em pesquisa de artigos a coisa mude um pouco; se quiser a sensação de jogo, recomendo procurar um livro de álgebra abstrata como Dummit and Foote; há um prazer bem de jogo em fazer provas, e para livros famosos costuma haver explicações online quando você trava
  • Talvez você esteja falando dos axiomas de Euclides, que definem um sistema com conceitos como ponto, reta, plano e paralelas; fora do plano, como sobre uma esfera, esse sistema quebra; ou talvez esteja se referindo à teoria dos conjuntos de Zermelo-Fraenkel (ZF/ZFC), sobre a qual a matemática moderna inteira é construída
  • Também existe um jogo chamado Bombe, uma variação de Campo Minado; em vez de abrir células diretamente, você joga criando regras sobre “quando é possível colocar uma bandeira”; conforme o nível sobe, as regras passam a encadear umas nas outras como lemas, e conforme o jogador melhora também dá para relaxar as restrições do conjunto de ferramentas e generalizar mais link do jogo
  • Matemática é essencialmente o processo de partir de axiomas e derivar conclusões; claro que não é só isso, mas no meu nível é assim que entendo
• Fazendo um pouco de preciosismo, é estranho dizer que o teorema two_eq_two parece uma função; como ele não tem argumentos, está mais para uma constante (embora eu saiba que constantes também sejam funções sem argumentos); acho mais convincente usar x_eq_x abaixo e então aplicá-lo em 2_eq_2 como se fosse uma função

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  Aqui x_eq_x realmente parece uma função, e em 2_eq_2 ela é usada dessa forma
  • É uma observação correta! Não fiz assim porque a forma como o Lean trata argumentos (especialmente conceitos como dependent types — dar x e receber a prova de x = x) ainda me parece um pouco estranha, e isso merece ser tratado à parte; vou falar disso no próximo artigo
• Uma dificuldade que senti ao aprender Lean é que as tactics (rfl e afins) são abrangentes demais, e mesmo com tutorial é difícil entender o significado exato; por exemplo, em C eu consigo rastrear mudanças de estado até o nível de bits, mas no Lean tudo parece meio nebuloso; e a sintaxe da tactic rewrite (rw) também me soa pouco natural
  • No Coq (agora Rocq) também sempre tive dificuldade de me adaptar às tactics; por exemplo, já passei pela situação de ter “A = B” e “P(A,A)” e querer transformar isso em “P(A,B)”, mas o rewrite não funcionava por motivos difíceis de explicar (imagino que por causa da definição da estrutura intermediária); por outro lado, o Metamath e o banco de dados set.mm fazem você provar tudo sem tactics, só com inferência explícita (usando regras como ax-mp), mas aí o problema é ter de decorar um monte de lemas utilitários, o que também não é simples
  • Esse é um dos motivos pelos quais prefiro Agda; Agda praticamente não tem tactics, e usando a correspondência Curry-Howard você escreve diretamente os termos de prova como numa linguagem de programação funcional; em compensação, se você for preguiçoso com abstração e criação de funções, até coisas triviais podem virar algo absurdamente trabalhoso, então disciplina importa muito
  • Pelo menos no Lean, dá para ir em “ir para a definição” das tactics e ver como elas funcionam por dentro; quando você está aprendendo, a quantidade de coisa é pesada, mas no fim tudo pode ser inspecionado (embora, chegando na teoria de tipos básica, fique mais difícil de intuir); e você comentou que a sintaxe de rewrite não parece natural, então fico curioso: o que seria uma sintaxe natural de rewrite para você?
  • Uma coisa que achei interessante é que as tactics ficam todas no nível “do usuário”, fora do kernel da prova; isso faz sentido, porque você quer manter um kernel pequeno e verificado sem mexer nele; mas isso também quer dizer que, quando as tactics são atualizadas ou alteradas, provas existentes podem quebrar; fico curioso sobre o quanto isso é um problema na prática
  • Ao contrário do que eu esperava, no Lean reflection e rewrite pareciam ser mais fundamentais do que adição; o Lean fornece adição pronta, mas parece que você precisa usar rfl ou rewrite toda vez; talvez exista algum tipo de prelude no Lean que automatize isso
• Queria saber se existe um jeito de ler proofs no Lean de forma não interativa; ao jogar o natural number game, achei muito difícil ler proofs que eram só uma sequência de comandos rw [x]; dá para ver o estado de cada linha no editor, mas ter de ficar clicando quebra o fluxo; seria como se em Python você não tivesse indentação e, para entender a estrutura de blocos, precisasse clicar em tudo; talvez isso seja uma impressão causada pelos comandos limitados do começo do jogo, mas queria saber se no ambiente completo do Lean isso melhora

  • Existe um jeito de ler provas no Lean de forma não interativa?
    Eu também fiquei curioso recentemente e fui procurar; o blog lean-in-latex mostra uma forma de acompanhar esse fluxo fora do editor e sem clicar, e também dá para ver como a comunidade Lean aborda isso

  • O Rocq antigamente tinha algo chamado “linguagem de prova matemática”; é difícil achar exemplos de uso real, mas a ideia era algo assim

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    Essa abordagem fazia a leitura parecer uma “prova escrita à mão” de artigo, mas quase ninguém usava e ela acabou sumindo; a linguagem de provas Isar, do Isabelle, é parecida e na verdade está mais próxima do estilo padrão; exemplo:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    Nele, a estrutura lógica geral e os resultados intermediários ficam explicitados com clareza, e só quando os detalhes importam menos você encurta com by ...; não sei se o Lean tem algo assim, mas pelo menos isso pode servir como palavra-chave de busca ou tema de pergunta nos fóruns do Lean
  • Ótima pergunta mesmo! Ainda sou iniciante, então não digo isso com total confiança, mas compartilho a sensação: depois de usar Lean por uns dois meses, percebi que ler código de prova é diferente de ler código de programação, e se parece mais com “escanear”; você presta atenção à estrutura geral do argumento, a quais tactics estão sendo usadas, a quais lemas aparecem; o estilo de código Lean costuma indentar a cada novo goal e desindentar quando o goal termina, então a forma do argumento importa bastante na leitura; veja por exemplo este meu PR; quando você se acostuma com tactics, passa a reconhecer que intro significa entrar em um quantificador, constructor significa dividir o goal, e por aí vai; no fim, tactics são macros/DSLs que constroem uma árvore de prova (term tree); quando olho código de prova, sinto como se estivesse vendo manipulações de árvore (quebrar em partes, preencher a ordem etc.); ainda assim, continua sendo verdade que, para saber exatamente qual é uma afirmação no meio da prova, muitas vezes você precisa clicar; uma prova com boa ideia pode ser lida com a clareza da progressão lógica de um artigo; por isso, quem quer comunicar intenção costuma usar nomes fáceis de ler, desenvolvimento claro, extração de lemas pequenos e o padrão de colocar as hipóteses primeiro e resolver com um código de prova curto; já partes que são mecanicamente chatas, mas óbvias para um matemático, costumam virar “golfing” (codificação minimalista); o estilo golf muitas vezes encurta o código, mas só trata de partes que o humano já entende intuitivamente; em resumo, no Lean a estrutura de leitura é implícita, mas há jeitos de deixá-la mais clara, e quanto mais você domina as tactics, mais consegue captar a estrutura sem clicar; só de bater o olho nos nomes dos lemas já dá para entender o fluxo geral, e a ordem pode ser reconstruída com facilidade
• O conteúdo ficou realmente muito bom; acho raro encontrar alguém que consiga explicar esse tipo de coisa de um jeito fácil de digerir; o segredo é mostrar todas as pequenas etapas que especialistas normalmente pulam
  • Obrigado!
• Queria saber se daria para ouvir opiniões nesta thread sobre o futuro de Lean vs idris/coq/agda; quero estudar representação de conhecimento, mas antes de me aprofundar em qualquer coisa fico preocupado com tamanho de comunidade e risco futuro; no passado já investi tempo em clojure core.logic e sofri com o problema de pouco interesse/ comunidade muito pequena, então agora tenho dificuldade de começar de novo
  • Pela minha experiência prática, Lean e Coq/Rocq são muito mais usados que Idris e Agda, e também têm bibliotecas e comunidades bem maiores; Rocq é muito usado para verificação de programas, o que acho que se deve à sua história mais longa, e ele tem várias peculiaridades, então o Lean talvez alcance isso em breve; Lean é o mais comum em prova de teoremas matemáticos; entre os projetos famosos de Rocq estão CompCert, CertiCoq e seL4, e há casos de uso em verificação de software aeronáutico de verdade (veja esta lista de projetos); no Lean há o mathlib (coleção de provas matemáticas), a formalização do último teorema de Fermat (projeto de prova do FLT) e o PFR, entre outros projetos grandes; pelo que sei, Idris e Agda não têm projetos de “mundo real” desse porte, embora eu possa estar enganado; de qualquer forma, o tamanho de todos eles ainda é muito pequeno comparado com linguagens ou comunidades como C++ ou JavaScript, e verificação de programas na prática é um trabalho muito lento e tedioso; talvez haja mudanças fundamentais no futuro com o avanço da IA, mas as habilidades aprendidas ainda devem continuar úteis
  • Acho que, na prática, não faz sentido apostar nesse campo; a maioria dos matemáticos de fato não tem grande interesse em formalização, por causa da distância entre uma prova escrita à mão e a sintaxe rígida que o computador exige; o melhor é encarar isso como algo divertido para aprender e praticar; em termos de perspectiva futura, o Lean parece o mais ativo recentemente, mas cada sistema tem sua base histórica de usuários, então é difícil prever
• Fico curioso se, sem nenhuma técnica especial ou truque, só de jogar coisas aleatórias no Lean e ver se o Lean aceita, dá para chegar a descobertas interessantes; ou se seria possível automatizar isso com um sistema automático ou LLM, tentando em massa proofs/teorias difíceis e vendo o que dá certo? Talvez a pergunta soe estranha, mas mal entendo Prolog
  • Do ponto de vista de alguém que trabalha profissionalmente com programação certificada, acho que IA generativa e métodos formais combinam muito bem; na verdade, eu diria que saber se LLMs vão substituir programadores depende bastante de quão bem a IA vai conseguir fazer programação certificada e raciocínio combinatório,

    Jogando coisas aleatórias dá para ter descobertas interessantes?
    IAs antigas iam bem em problemas com poucos estados possíveis, como damas; xadrez já é um pouco mais difícil, e go era praticamente impossível para IA tradicional sem aprendizado de máquina; linguagens formais têm um número de estados possíveis e caminhos de busca absurdamente grande; quando a natureza do problema é clara, dá para usar SMT solvers em força bruta; originalmente SMT solvers e proof assistants eram áreas diferentes dentro de métodos formais, mas hoje eles se complementam cada vez mais (veja Sledgehammer e Lean-SMT)
    E se LLMs ou sistemas automáticos tentassem proofs/teorias arbitrárias?
    Isso ainda não é pesquisa totalmente mainstream, mas já houve e há bastante trabalho nessa direção; mesmo antes do boom dos LLMs, grandes financiadores já apoiavam isso havia anos; houve tentativas antigas como “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies”, e pesquisas mais recentes como DeepSeek-Prover; ainda está totalmente em aberto como treinar bem esses sistemas e até onde vai o potencial deles,
    Na prática, os LLMs atuais ainda deixam bastante a desejar em linguagens como Rocq e Lean, e quando produzem uma resposta errada, corrigi-la é muito doloroso; ainda assim, espero que o nível das ferramentas de IA melhore bastante com o tempo

  • Esta é realmente uma área de pesquisa e experimentação muito ativa!
    A comunidade Lean se reúne bastante no Zulip, e no canal Machine-Learning-for-Theorem-Proving dá para encontrar várias threads de referência
• Vim a me interessar pelo Lean pela primeira vez por causa do alphaproof, e achei o texto introdutório excelente; você poderia contar em que está mexendo no Lean?
  • Por enquanto estou só estudando matemática com Lean; mais especificamente, estou seguindo o material do Tao para Lean e preenchendo eu mesmo os trechos sorry que faltam nos exercícios (minhas soluções estão aqui)
• Queria saber se no Lean existe algum modo de verificação que impeça automaticamente o uso de provas não confiáveis (proof com sorry) ou a adição contínua de novos axiomas; por exemplo, dá para confirmar algo como “esta prova não usa sorry de jeito nenhum” ou “ela depende apenas do poder de prova de um conjunto fixo de axiomas”?
  • Acho que o #print axioms some_theorem mencionado mais para o fim do artigo talvez seja justamente um exemplo disso; com ele dá para ver se a prova depende direta ou indiretamente de sorry ou de axiomas não revisados
  • Com print axioms dá para verificar se não há axiomas adicionais, e também observar se compila sem warnings nem erros; o utilitário SafeVerify também pega alguns truques encontrados por sistemas de RL
  • Também existe conteúdo aqui mostrando que isso também é possível com macros