A structured path from zero Lean knowledge to AI-assisted theorem proving.

This repository is a hands-on learning environment for Lean 4, designed for mathematicians and programmers who want to master interactive theorem proving and engage with the cutting edge of AI-integrated formal mathematics. The roadmap is aligned with the research themes of the Harmonic Aristotle program and the broader goal of Mathematical Superintelligence (MSI).

If you've never used Lean before, you're in the right place. This repo is designed so that you can open any file, read it top to bottom, and learn by doing. Every concept is introduced with explanations, examples, and exercises.

Three rules for success:

1. Read the Lean Infoview — The panel on the right side of VS Code is your window into Lean's mind. Always look at it as you move your cursor through a proof.
2. Try before you peek — Every sorry is an exercise. Attempt it yourself before searching for hints. Struggling is how you build intuition.
3. Experiment fearlessly — Use Sandbox.lean to try wild ideas. You can't break anything; Lean will just tell you if something is wrong.

Lean 4 is both a programming language and a proof assistant. It lets you write executable programs AND machine-checked mathematical proofs — in the same language.

This is the Curry-Howard correspondence, and once it clicks, everything else follows naturally:

Why does this matter? It means that when you prove a theorem in Lean, the computer can check your proof mechanically. No hand-waving allowed. And when AI systems like Aristotle or AlphaProof generate proofs, Lean can verify them with 100% certainty.

• Largest mathematical library: Mathlib has 200,000+ formalized theorems and growing
• Best AI tooling: LeanDojo, Pantograph, LeanCopilot — the ecosystem AI researchers use
• Active community: The Lean Zulip chat is welcoming and responsive
• Modern language: Lean 4 is fast, has a real compiler, and feels like a modern programming language
• Industry momentum: Aristotle, AlphaProof, DeepSeek-Prover — all use Lean 4

• A code editor: VS Code is strongly recommended (Lean's tooling is built for it)
• Basic programming experience: If you've written functions in any language, you're ready
• Mathematical curiosity: Undergraduate-level math helps, but isn't strictly required for the early phases

Step 1 — Install Lean 4 via elan (the Lean version manager):

# Linux / macOS
curl https://elan.lean-lang.org/install.sh -sSf | sh

# Windows: download the installer from https://lean-lang.org/lean4/doc/setup.html
# After installing, you may need to add elan to your PATH:
#   setx Path "%USERPROFILE%\.elan\bin;%Path%"
# Then restart your terminal.

Step 2 — Install VS Code + the lean4 extension:

1. Download VS Code
2. Open VS Code → Extensions (Ctrl+Shift+X) → search "lean4" → Install
3. The extension provides syntax highlighting, the Infoview panel, and error diagnostics

Step 3 — Clone and build this project:

git clone https://github.com/omegaestable/lean.git
cd lean
lake update    # Downloads Mathlib (~3 GB the first time — be patient!)
lake build     # Compiles the project (takes a while the first build)

Tip for Windows users: If lake is not recognized, make sure %USERPROFILE%\.elan\bin is on your PATH. You can set it temporarily with:

$env:Path = "$env:USERPROFILE\.elan\bin;" + $env:Path

Step 4 — Open in VS Code and explore!

Open the lean folder in VS Code. Open any .lean file. The Lean Infoview panel will appear on the right — this shows proof states, types, and errors in real time.

Your most important tool is the Infoview panel. Place your cursor on different lines of a proof and watch the panel update. This is how you "see" what Lean is thinking.

The repo is organized into 5 phases, each building on the previous. Files are numbered so you can work through them in order.

LeanLab/
│
├── Basics/                          ← PHASE 1: Lean Fundamentals
│   ├── HelloWorld.lean                 01 — #check, #eval, your first theorem
│   ├── TypesAndTerms.lean              02 — Types, Prop vs Type, inductive types
│   └── Functions.lean                  03 — Recursion, pattern matching, higher-order
│
├── Logic/                           ← PHASE 1 (continued): Proof Skills
│   ├── PropositionalLogic.lean         04 — ∧, ∨, →, ¬, ↔ (Curry-Howard in action)
│   ├── Quantifiers.lean                05 — ∀, ∃, equality, classical logic
│   └── Tactics.lean                    06 — Full tactic reference + practice
│
├── Mathlib/                         ← PHASE 2: Library Mastery
│   ├── SearchAndDiscovery.lean         07 — exact?, apply?, naming conventions, Loogle
│   └── WorkingWithMathlib.lean         08 — Typeclasses, proof engineering, contributing
│
├── Metaprogramming/                 ← PHASE 3: Extending Lean
│   ├── CustomTactics.lean              09 — TacticM monad, custom tactics, Expr type
│   └── MacrosAndDSLs.lean             10 — Macros, syntax extensions, elaboration
│
├── Mathematics/                     ← PHASE 4: Real Formalization
│   ├── NaturalNumbers.lean             11 — Induction, divisibility, modular arithmetic
│   ├── Algebra.lean                    12 — Groups, rings, fields via Mathlib
│   └── Analysis.lean                   13 — Sequences, metric spaces, ε-δ proofs
│
├── AIIntegration/                   ← PHASE 5: AI + Lean
│   ├── Overview.lean                   14 — Landscape, proof states, training data
│   ├── Autoformalization.lean          15 — Informal→formal, pitfalls, pipelines
│   └── ToolsSetup.lean                16 — LeanDojo, Pantograph, LeanCopilot setup
│
├── Exercises/                       ← Progressive Difficulty
│   ├── Level1_Basics.lean              ⭐ Functions and simple proofs
│   ├── Level2_Logic.lean               ⭐⭐ Propositional and predicate logic
│   ├── Level3_Math.lean                ⭐⭐⭐ Algebra, inequalities, induction
│   ├── Level4_Competition.lean         ⭐⭐⭐⭐ AMC/AIME/IMO-style problems
│   └── Level5_Research.lean            ⭐⭐⭐⭐⭐ Research-level formalization
│
└── Sandbox.lean                     ← Your playground — experiment freely!

• If you're brand new to Lean: Start with Basics/HelloWorld.lean. Read every comment. Move your cursor through the file and watch the Infoview.
• If you know some programming: Skim through Basics/, then spend time on Logic/PropositionalLogic.lean.
• If you know some proof assistants: Jump to Mathlib/SearchAndDiscovery.lean and Mathematics/.
• If you're here for AI/Lean: Read everything in order — the foundations matter for understanding how AI systems interact with Lean.

Goal: Fluency in Lean 4 syntax, types, and interactive proof.

Think of this phase as learning to read and write in a new language. You need to be comfortable with the basic vocabulary (types, functions, propositions) before you can express complex ideas (theorems, proofs).

Parallel activity: Complete the Natural Number Game — it's the best interactive introduction to Lean proofs. Also start reading Theorem Proving in Lean 4.

Goal: Navigate and use Mathlib, the world's largest formalized math library.

Mathlib has 200,000+ lemmas. Nobody memorizes them. The skill you're building here is how to FIND what you need — this is also exactly what AI models need to learn (premise selection).

Parallel activity: Work through Mathematics in Lean. Explore Tao's Lean companion to Analysis I. Join the Lean Zulip.

Goal: Extend Lean itself with custom tactics, macros, and automation.

This is where you go from being a Lean USER to a Lean BUILDER. The same APIs used here are what LeanDojo and Pantograph use under the hood — so understanding metaprogramming is essential for AI/Lean work.

Parallel activity: Read the Lean 4 Metaprogramming Book. Explore LeanDojo and PyPantograph source code.

Goal: Formalize real math, then connect it to AI toolchains.

Now you bring everything together. The Mathematics files show you what "real" formalization looks like — not toy examples, but actual mathematical structures and proofs. The AI Integration files show you how AI systems interact with these proofs.

Parallel activity: Study the Aristotle, DeepSeek-Prover, and FORMAL papers.

Goal: Original contributions, collaborations, and Aristotle grant preparation.

Not sure where to begin? Here's a concrete plan:

1. Open LeanLab/Basics/HelloWorld.lean in VS Code
2. Read the top comment — it explains what Lean is and how to read the file
3. Place your cursor on #check 42 — look at the Infoview panel on the right. It should say 42 : Nat
4. Move your cursor to #eval 2 + 3 — the Infoview shows 5
5. Find theorem two_plus_two — put your cursor on rfl and read what the Infoview says
6. Scroll to "TRY IT YOURSELF" — replace sorry with rfl and see the error disappear
7. Celebrate! — you just proved your first theorem

When you're done with HelloWorld, move to TypesAndTerms.lean, then Functions.lean, and so on.

The Harmonic Aristotle program offers Principal Investigator Awards (~$100K) and Rising Mathematician Awards for work advancing Mathematical Superintelligence. Key themes:

1. Autoformalization & Retrieval: RAG/RAT systems for Lean 4, agentic feedback loops, benchmark curation
2. Proof Search & RL: MCTS/MCGS strategies, value models, test-time training
3. Datasets & Benchmarks: Correcting misformalizations, creating new benchmarks, evaluation metrics
4. Model Fine-tuning: LoRA on Lean proof data, premise selection, local deployment
5. Human-AI Collaboration: Mixed-initiative interfaces, interpretable suggestions

Full reference: CHEATSHEET.md

Q: I've never used a proof assistant before. Is this for me? Yes! Phase 1 assumes no prior Lean knowledge. If you can write a function in any programming language, you can learn Lean. The hardest part is the first week — after that, patterns emerge and it gets much more natural.

Q: Why Lean 4 and not Coq/Isabelle/Agda? Lean 4 has the most active mathematical library (Mathlib, 200K+ theorems), the strongest AI tooling ecosystem (LeanDojo, Pantograph, LeanCopilot), and a welcoming community. It's the platform of choice for Aristotle, AlphaProof, and most recent AI/Lean research.

Q: What's sorry? A placeholder meaning "proof goes here." Every sorry in this repo is an exercise for you. Your job is to replace them with real proofs. A file with zero sorrys is fully proven. The Lean compiler will show a warning for every sorry — that's by design!

Q: How do I find lemmas in Mathlib? Use exact? / apply? / rw? inside proofs (they search automatically). Use Loogle for type-based search. Use Moogle for natural language search. See Mathlib/SearchAndDiscovery.lean for a full guide.

Q: I'm stuck on a proof. What do I do?

1. Read the Infoview — what's the current goal? What hypotheses do you have?
2. Try the power tactics: exact?, simp, omega, ring, aesop, linarith
3. Use #check to explore related lemmas
4. Simplify the problem — can you prove a special case first?
5. Ask for help on Lean Zulip — the community is very friendly

Q: How long does it take to get comfortable with Lean? Most people feel productive after 2–4 weeks of regular practice. Fluency with Mathlib takes longer (2–3 months). Metaprogramming is its own learning curve. Be patient with yourself — even experienced mathematicians find the first week challenging.

Q: How do I start with AI/Lean tools? See AIIntegration/ToolsSetup.lean. Start with pip install lean-dojo and extract proof data from your own files. This connects your Lean work to the AI pipeline.

Q: Can I use this repo for a course or study group? Absolutely! The exercises are designed to be progressive. Level 1–2 work well for a week-long workshop. Level 3–4 can fill a semester project.

• Lean Zulip Chat — main community hub, very welcoming to beginners
• Mathlib Initiative — strategic support for the Mathlib ecosystem
• Lean FRO — Lean Focused Research Organization
• Harmonic — Aristotle program and AI/Lean research
• Lean 4 Dev — comprehensive learning platform

This project is open source. Use it, share it, learn from it, build on it.