Learning Lean: Part 1

The author, a mathematician turned software engineer, embarks on a journey to learn the Lean theorem prover, captivated by the movement to formalize mathematics. This initial post details their early experiences and the foundational concepts that proved challenging from a programming language perspective. They advocate for formalization not just for error detection but also for enabling clearer separation of concerns in mathematical exposition, allowing human-centric explanations to flourish while mechanical proofs are verified by tools.

• Motivation for Formalization: Beyond error catching and reducing trust, Lean allows mathematicians to focus written exposition on intuition and motivation, leaving mechanical verification to the tool. This separation is crucial for training future AI systems to understand mathematical thought processes.
• Future of Math with AI: The author envisions a two-tiered collaboration where AI helps explore high-level proof strategies, Lean builds formal proofs, and human papers narrate the "spark of genius" distinct from symbol-following.
• Author's Background: A PhD mathematician with 15 years in software engineering (frontend) and a deep interest in programming languages, but lacking formal training in PL theory, type theory, or logic. This unique background informs the perspective on Lean's learning curve.
• Dependent Type Challenges: The core hurdles included understanding Lean's three-level object hierarchy (terms, types, universes), the disorienting homoiconicity of types and terms, and the subtle distinction between optional argument names and optional types in function signatures.
• Numeric Literals & Type Classes: Similar to early Haskell experiences, the treatment of numeric literals as type class objects presented an initial barrier, feeling "inverted" for newcomers expecting simpler behavior.
• Curry-Howard in Practice: While theoretically proving programs and proofs are the same, in practice, they diverge into Prop and Type universes, with proof-specific constructs (tactics, implicit arguments) necessary for developer experience that wouldn't typically suit general computational programs.
• Lingering Questions: The author concludes with open questions regarding definitional equality, the Prop vs Decidable distinction, #eval vs #reduce, and the comparative power of Lean's simp vs. CAS like Mathematica.

Despite the initial oddities of a dependently typed language, the author expresses awe at Lean's power to construct all of known mathematics from a small set of foundational concepts. They are now ready to progress to "Mathematics in Lean," acknowledging the invaluable support from the Lean Zulip community.