Learning Lean: Part 1
4 days ago
- #formal mathematics
- #dependent types
- #Lean theorem prover
- The author is motivated by the movement to popularize mathematics formalization using Lean, highlighting its benefits like error detection and reduced need for trust among collaborators.
- Formalization allows mathematicians to focus on intuition and motivation in their writing, rather than mechanical verification of details, which is especially valuable in the era of Large Language Models (LLMs).
- The author envisions future collaboration between mathematicians and AI, where AI helps with high-level proof strategies and Lean handles formal proofs, leading to papers that focus on the 'story' of the proof.
- The author shares their background: a PhD in mathematics with a focus on algebra, number theory, and combinatorics, followed by a career in software engineering, particularly in web front-end development.
- The author discusses the challenges of learning Lean, especially due to the need for understanding foundations like type theory and logic, which are less familiar to many mathematicians.
- The author compares learning Lean to engaging with a classic foreign language text, requiring knowledge of multiple deep and independent bodies of knowledge.
- The author completed the Natural Number Game and the Set Game online, which provided a good introduction to Lean.
- The author describes the three-level hierarchy in Lean: terms, types, and universes, and the challenges of understanding their interactions.
- The author notes the syntactic confusion in Lean due to the blending of type and term worlds, unlike in languages like TypeScript where they are more distinct.
- The author discusses the optional naming and typing in Lean, which can be confusing for beginners.
- The author shares their initial struggles with numeric literals and type classes in Lean, drawing parallels to their early experiences with Haskell.
- The author reflects on the practical differences between theory and practice in Lean, particularly the separation of Prop and Type universes.
- The author lists remaining questions about Lean, including definitional equality, Prop vs Decidable, and the difference between #eval and #reduce.
- The author expresses awe at how Lean, with its small set of foundational constructs, can build all of known mathematics.
- The author thanks the Lean Zulip community for their help and mentions using Claude for simpler questions but relying on experts for more complex ones.