lean-lab

Self-taught Lean 4 formalization log — learning in public, one small proof at a time. Every committed file is machine-checked (lean <file> → no errors, no sorry).

These are known results, re-derived for practice — no novelty is claimed. Cantor's theorem and Lawvere's fixed-point theorem are already in mathlib / agda-unimath; Rice's theorem and the halting problem are in mathlib too. This repo is a learning trace, not a contribution.

The through-line is the diagonal / no-go argument: how "impossible" gets proved — from the basics up to the abstraction that unifies Cantor, Gödel, Turing, and Rice.

Basics

• grain1.lean — a first rw proof beyond ring/decide.
• zero_add.lean — 0 + n = n by induction.
• zero_add_simp.lean — the same fact via simp.

No-go / impossibility (the diagonal theme)

• no_largest.lean — there is no largest natural number.
• not_surjective_succ.lean — the successor function is not surjective.
• cantor.lean — Cantor's diagonal theorem: no f : X → (X → Bool) is surjective.
• lawvere.lean — Lawvere's fixed-point theorem (the abstraction of the diagonal); Cantor falls out as a one-line corollary.