lean-formalization

name	lean-formalization
description	Lean 4 formalization workflow for Erdős problem proofs. Use when formalizing a solution in Lean 4, checking existing formalizations, or setting up the Lean environment for proof verification.

Lean 4 Formalization Workflow

A structured approach to formalizing Erdős problem proofs in Lean 4, from assessing formalization feasibility through verified compilation and upstream contribution.

Quick Start

from tools.query_db import ErdosDB

with ErdosDB() as db:
    p = db.get_problem("42")
    print(p.lean_url)  # Check formalization status

# Build the local Lean project
cd lean && lake build

Phase 1: Assessment

Before attempting formalization, determine what already exists.

1.1 Check the Problem's Lean Status

from tools.query_db import ErdosDB

with ErdosDB() as db:
    p = db.get_problem("{number}")
    lean_url = p.lean_url

    if lean_url is None:
        print("No Lean link — formalization from scratch")
    elif "/blob/" in lean_url or lean_url.endswith(".lean"):
        print(f"Specific .lean file: {lean_url}")
    else:
        print(f"Generic repo link: {lean_url}")

1.2 Three Categories

Category	Count	What It Means
Specific .lean URL	~355	DeepMind has a formal statement — read it first
Generic repo URL	~824	Repo exists but no specific file — likely no formalization
No lean_url	remaining	No formalization link at all

1.3 Decision Table

Lean Status	Proof Grade (A-F)	Action
Specific .lean URL	A or B	Formalize — statement exists, add proof
Specific .lean URL	C or below	Skip formalization — proof not rigorous enough
Generic/No URL	A	Consider writing statement + proof from scratch
Generic/No URL	B or below	Skip — not worth formalizing without existing statement

Phase 2: Environment Setup

2.1 Use the Local Lean Project

The repository includes a Lean 4 project at lean/:

cd lean
lake exe cache get   # Download prebuilt mathlib (~1 min)
lake build           # Compile all files
./check_proofs.sh    # Verify the proofs are actually complete

Never run lake update. It regenerates lake-manifest.json and discards the pinned dependency revisions, so builds stop being reproducible. The manifest is committed deliberately. Skipping lake exe cache get means compiling mathlib from source — hours instead of a minute.

See lean/README.md for full setup instructions.

2.2 Project Structure

lean/
  ├── lean-toolchain          # Lean version (must match formal-conjectures)
  ├── lakefile.toml            # Package config + mathlib dependency
  ├── lake-manifest.json       # Dependency lock file (committed on purpose)
  ├── check_proofs.sh          # Axiom-level verification
  ├── ErdosProofs.lean         # Root import file
  └── ErdosProofs/
        ├── Audit.lean         # Fails the build on any unproved declaration
        ├── Template.lean      # Template for new proofs
        ├── PrimeGaps.lean     # Worked example of a complete proof
        ├── P{number}.lean     # Individual problem proofs
        └── Conjectures/       # Open problems, deliberately unproved

Completed proofs go directly under ErdosProofs/ and must be axiom-clean. A statement of a problem that is still open goes in ErdosProofs/Conjectures/, where sorry is expected and reported rather than failed.

2.3 Optional: lean-lsp-mcp

If available, the lean-lsp-mcp MCP server provides interactive type-checking and goal state inspection directly in Claude Code.

Phase 3: Statement Formalization

3.1 Read the Existing Statement

If a specific .lean URL exists, fetch the formal statement from formal-conjectures:

# The lean_url typically points to:
# https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/{file}.lean

Key things to extract:

• The theorem or conjecture declaration
• Type signatures (what's being quantified over)
• Imported mathlib modules
• Any custom definitions

3.2 Translate Definitions

Map informal math to Lean/mathlib types. See LEAN_PATTERNS.md for the full type mapping table.

Common translations:

• "For all integers n" → ∀ n : ℤ
• "There exists a prime p" → ∃ p : ℕ, Nat.Prime p ∧ ...
• "The set of primes" → {p : ℕ | Nat.Prime p}
• "Arithmetic progression" → ArithmeticProgression or explicit formulation

3.3 Verify Interpretation

Cross-check:

1. Does the Lean statement match the LaTeX from the database?
2. Do the quantifiers match? (∀ vs ∃, bounded vs unbounded)
3. Are there implicit assumptions made explicit in the formalization?

Phase 4: Proof Translation

4.1 Start with sorry

theorem erdos_problem_42 : <statement> := by
  sorry

Verify the statement compiles before writing any proof.

4.2 Incremental Construction

Replace sorry one step at a time:

theorem erdos_problem_42 : <statement> := by
  intro n hn
  -- Step 1: establish base property
  have h1 : <intermediate> := by
    sorry
  -- Step 2: apply key lemma
  sorry

Build after each step to catch type errors early.

4.3 Common Tactic Patterns

See LEAN_PATTERNS.md for the full tactic cheat sheet. Quick reference:

Proof Step	Lean Tactic
Case split	rcases, obtain, by_cases
Induction	induction n with, strong_induction_on
Rewriting	rw, simp, ring
Contradiction	by_contra, absurd, omega
Existential	use, exact ⟨_, _⟩, refine ⟨?_, ?_⟩
Finishing	exact?, apply?, omega, norm_num, decide

Phase 5: Iteration

5.1 Build-Check Loop

cd lean
lake build   # Check for errors

Common issues and fixes:

Error	Fix
unknown identifier	Missing import — check import Mathlib.X.Y
type mismatch	Wrong type — check #check on terms
unsolved goals	Proof incomplete — add more tactics
declaration uses sorry	Still has sorry — keep going
failed to synthesize	Missing instance — add [inst : Class]

5.2 Debugging with #check and #print

#check Nat.Prime           -- See the type
#print Nat.Prime           -- See the definition
#check @Finset.sum         -- See implicit arguments
example : 2 + 2 = 4 := by norm_num  -- Quick sanity check

5.3 When to Bail Out

Stop formalizing if:

• The proof relies on results not in mathlib (need custom theory development)
• Type-level encoding of the problem is unclear or disputed
• More than 3 build-fix cycles without progress on the core argument
• The informal proof has a gap that becomes apparent during formalization

Document what you achieved and what blocked progress.

Phase 6: Verification & Submission

6.1 Local Verification

cd lean
./check_proofs.sh   # exit 0 only if every proof is genuinely complete

A clean lake build proves nothing on its own. A theorem closed with sorry compiles; the warning is easy to miss on an incremental build; and sorry is contagious — a fully-written proof that cites a lemma containing sorry is itself unproved, and grepping your own file for "sorry" will not reveal it.

check_proofs.sh runs the real check: it walks the transitive axiom dependencies of every declaration and accepts a proof only if it rests on at most propext, Classical.choice and Quot.sound. Anything reachable from a sorry carries sorryAx and fails with exit code 1.

Check that:

• ./check_proofs.sh exits 0
• The audit counts your theorem among the proved declarations, not the open statements
• No unexpected axioms were reported
• Imports are minimal
• The file states plainly what it does and does not prove — if it proves a weaker or special case, say so in the module docstring

6.2 Contribute Upstream

If the proof is for a problem in formal-conjectures:

# Fork and clone
git clone https://github.com/{you}/formal-conjectures
cd formal-conjectures
lake exe cache get && lake build  # Verify clean build

# Add proof file
# Edit FormalConjectures/ErdosProblems/{file}.lean

# Test
lake build

# Submit PR

6.3 Update Local Documentation

After successful formalization:

1. Add the proof file to lean/ErdosProofs/P{number}.lean
2. Add the import to lean/ErdosProofs.lean
3. Note the formalization in your solution document

### Lean Formalization
- File: `lean/ErdosProofs/P{number}.lean`
- Status: passes `./check_proofs.sh` — axiom-clean, no `sorry` anywhere in the
  dependency chain
- Axioms: propext, Classical.choice, Quot.sound
- Proves exactly: [state the formal claim, and any way it is weaker than the
  informal problem]
- Upstream PR: [link if submitted]

Checklist Summary

□ Phase 1: Assessment
  □ Checked lean_url via SDK
  □ Categorized: specific file / generic link / none
  □ Decision: formalize or skip

□ Phase 2: Environment
  □ lake exe cache get (never lake update)
  □ lean/ project builds (lake build)

□ Phase 3: Statement
  □ Read existing formal statement (if any)
  □ Type mappings verified
  □ Statement matches informal problem

□ Phase 4: Proof
  □ sorry-stub compiles
  □ Incremental construction
  □ All sorry removed

□ Phase 5: Iteration
  □ lake build passes
  □ Type errors resolved

□ Phase 6: Verification
  □ ./check_proofs.sh exits 0
  □ Theorem counted as proved, not as an open statement
  □ No unexpected axioms
  □ Module docstring says what is and is NOT proved
  □ Upstream PR (if applicable)
  □ Local docs updated