Introduction to Lean for Programmers — source summary
A Towards Data Science tutorial by Ronen Lahat (19 May 2026) introducing the
lean-theorem-prover to a programming audience. Delivered via Telegram, ingested
2026-05-29. Capture in raw/lean-for-programmers.md (WebFetch; direct fetch was
Cloudflare-blocked).
What it covers
- Lean as an interactive proof assistant (checks legality of proof steps; helps build them) vs. automatic theorem provers.
- The Curry-Howard correspondence — “propositions are types, proofs are terms” — with a curried-function / vending-machine analogy, shown in TypeScript and Lean.
- Core machinery: dependent types, universe levels (paradox avoidance), propositions
as types,
rfl, and tactics (intro,cases,rw,simp,ring,omega, …), likened to learning SQL constructs. - AI-math context: LeanDojo, miniF2F, ProofNet, and DeepMind’s alphaproof (IMO silver-medalist) all build on Lean.
- History: Leibniz → Hilbert → Gödel → Church-Turing; why full proof automation is impossible, so assistants check rather than find.
Cluster note
Sits in a new cluster E (formal methods / theorem proving) — its own domain, but with an honest bridge to cluster A: see lean-theorem-prover for the “mechanizing reasoning” lineage that also runs through as-we-may-think.