All Lean Books And Where To Find Them

Summary

This partial ingest covers Evgenia Karunus’s curated guide to Lean books and learning paths. The source is not a formal Lean reference, but it is a useful routing note for the wiki because it distinguishes Lean as a programming language, a proof-assistant environment, a metaprogramming platform, and a mathematics-formalization ecosystem.

The guide is also a practical bridge between the wiki’s logic pages and proof-assistant work: it highlights resources on proof terms, tactics, inductive definitions, structures, type hierarchies, Mathlib-style formalization, and Lean metaprogramming.

Key Claims

• Lean learners often need several resources because Lean combines functional programming, theorem proving, tactic scripting, and formal mathematics.
• “Functional Programming in Lean” is positioned as the route into Lean as a normal programming language, especially for understanding structure, inductive, and instance search.
• “Theorem Proving in Lean” is treated as the central repeated resource because it explains proof terms, tactics, inductive types, recursors, and Lean’s Calculus-of-Constructions-style basis.
• “Mathematics in Lean” and “Formalising Mathematics” are framed as hands-on paths for writing Mathlib-style proofs and formalizing mathematics.
• “Metaprogramming in Lean” and tactic tutorials are separate advanced resources for users who want to write tactics or work with Lean internals.
• “Logic and Mechanized Reasoning” is described as a logic and SAT/SMT implementation path in Lean rather than a tactic-proof tutorial.

Methods / Formalism

• The source’s technical anchors are Lean proof terms and tactics. A proof term such as:

And.intro (And.right h) (And.left h)

constructs a proof object directly, while tactic scripts elaborate to proof terms checked by Lean.

• The guide repeatedly marks structure, inductive, recursors, type-class instance search such as [Group G], and metaprogramming APIs as the objects one must understand to move from surface proofs to Lean internals.
• The source reports that Lean is based on a Calculus of Constructions with inductive types; Lean Theorem Prover keeps the wiki’s compact technical anchor for that claim.
• See Lean Proof Terms and Tactics for the focused proof-term/tactic annex.

Evidence / Experiments

• This is a subjective resource guide, not a benchmark, formal proof, or literature survey.
• It is useful as navigational evidence about the Lean learning ecosystem and as a reminder of which technical objects recur across Lean books.
• The current ingest reviewed the clipped page and checked the live page header for the author name.

Connections

• Seeds Lean Theorem Prover as the wiki concept for Lean’s proof-assistant role.
• Adds Lean Proof Terms and Tactics as the formal annex for proof judgments, direct proof terms, and tactic elaboration.
• Connects to Higher-Order Logic and Intuitionistic Logic through typed proof objects, propositions-as-types, and constructive proof workflows.
• Extends Formal Methods with a proof-assistant route alongside automata, temporal logic, synthesis, and model checking.
• Complements Vaananen2024 - Second-Order and Higher-Order Logic by showing the practical proof-assistant side of higher-order/type-theoretic logic.

Open Questions

• Should the wiki later ingest the primary Lean documentation, “Theorem Proving in Lean”, or “Functional Programming in Lean” as canonical technical sources?
• Should Lean Theorem Prover remain a specific concept page, or should a broader proof-assistants page be split out after more sources arrive?
• Which formalization examples in the existing wiki would be worth encoding in Lean?

Citation

Karunus, Evgenia. 2026. “All Lean Books And Where To Find Them.” https://lakesare.brick.do/all-lean-books-and-where-to-find-them-x2nYwjM3AwBQ.