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