Learn Math by Lean Notebook
Create a real .ipynb tutorial for a user-chosen mathematics topic using Lean 4 and mathlib as the executable medium. Match the rhythm of a theory-practice notebook: explain one idea, run or inspect a small Lean fragment, then build toward a modest theorem or proof pattern.
Default to Chinese prose when the user writes in Chinese, English prose when the user writes in English, and bilingual prose only when the user asks for it or says "中英文", "bilingual", or similar. Lean code, theorem names, identifiers, comments, and error labels should stay in English.
Workflow
- Infer the topic, target level, and requested language. If unclear, assume a curious beginner who can read basic Lean syntax.
- Read
references/notebook-style.md before generating a notebook unless the task is only a quick outline.
- Choose one concrete end point: a formalized theorem, a reusable proof pattern, a small computation, a structure/API tour, or a Lean/mathlib translation of a familiar mathematical argument.
- Build the notebook as a sequence:
- Title cell with the topic and language-appropriate subtitle.
- Environment cell explaining the expected Lean 4/Jupyter setup.
- Roadmap cell with 3-6 steps.
- Concept blocks: short math explanation, then a focused Lean cell.
- Proof blocks: definitions or examples first, lemmas next, final theorem last.
- Debugging blocks: common Lean errors and how to read them.
- Exercises: 3-5 small modifications or proofs.
- Save a valid
.ipynb file. Prefer notebook-native JSON over prose-only drafts when the user asks to create the notebook.
When the user asks to register, create, debug, or document a project-specific Lean 4 Jupyter kernel, use scripts/register_lean4_jupyter_kernel.py as the canonical helper and read the kernel registration section in references/notebook-style.md.
Notebook Rules
- Keep markdown cells short. Do not write a textbook chapter before the first Lean cell.
- Put every abstract idea near a runnable Lean example,
#check, #eval, example, lemma, or theorem.
- Prefer mathlib's existing names and APIs. Use
#check, #find, or local search when working in a real Lean project.
- Avoid fake Lean. If a proof is likely hard, mark it as an exercise or use an honest intermediate theorem instead of inventing unsupported code.
- Keep code cells focused. One cell should introduce one definition, API, proof move, or theorem.
- Use comments only where they orient the learner.
- Include expected outcomes in markdown near cells that may require an external Lean kernel.
Lean Style
- Use Lean 4 syntax:
fun x => ..., <| when it improves readability, and no empty lines inside declarations.
- Name examples and lemmas in English when names matter.
- Prefer small proofs with
by, simp, rw, ring, omega, linarith, and explicit intermediate lemmas when appropriate.
- Do not hide hard formalization gaps behind
set_option maxHeartbeats.
Bundled Reference
Read references/notebook-style.md for the recommended notebook shape, language modes, Lean cell patterns, and validation checklist.
1---2name: learn-math-by-lean-notebook3description: Generate Jupyter notebooks that teach mathematics through Lean 4 and mathlib by interleaving compact bilingual-capable explanations, runnable Lean code cells, proof experiments, and small exercises. Use when the user asks to learn a math topic with Lean, wants a Lean 4/mathlib tutorial notebook, requests Chinese or English math-learning notebooks, or wants a theory-plus-formalization lesson in .ipynb form.4---56# Learn Math by Lean Notebook78Create a real `.ipynb` tutorial for a user-chosen mathematics topic using Lean 4 and mathlib as the executable medium. Match the rhythm of a theory-practice notebook: explain one idea, run or inspect a small Lean fragment, then build toward a modest theorem or proof pattern.910Default to Chinese prose when the user writes in Chinese, English prose when the user writes in English, and bilingual prose only when the user asks for it or says "中英文", "bilingual", or similar. Lean code, theorem names, identifiers, comments, and error labels should stay in English.1112## Workflow13141. Infer the topic, target level, and requested language. If unclear, assume a curious beginner who can read basic Lean syntax.152. Read `references/notebook-style.md` before generating a notebook unless the task is only a quick outline.163. Choose one concrete end point: a formalized theorem, a reusable proof pattern, a small computation, a structure/API tour, or a Lean/mathlib translation of a familiar mathematical argument.174. Build the notebook as a sequence:18 - Title cell with the topic and language-appropriate subtitle.19 - Environment cell explaining the expected Lean 4/Jupyter setup.20 - Roadmap cell with 3-6 steps.21 - Concept blocks: short math explanation, then a focused Lean cell.22 - Proof blocks: definitions or examples first, lemmas next, final theorem last.23 - Debugging blocks: common Lean errors and how to read them.24 - Exercises: 3-5 small modifications or proofs.255. Save a valid `.ipynb` file. Prefer notebook-native JSON over prose-only drafts when the user asks to create the notebook.2627When the user asks to register, create, debug, or document a project-specific Lean 4 Jupyter kernel, use `scripts/register_lean4_jupyter_kernel.py` as the canonical helper and read the kernel registration section in `references/notebook-style.md`.2829## Notebook Rules3031- Keep markdown cells short. Do not write a textbook chapter before the first Lean cell.32- Put every abstract idea near a runnable Lean example, `#check`, `#eval`, `example`, `lemma`, or `theorem`.33- Prefer mathlib's existing names and APIs. Use `#check`, `#find`, or local search when working in a real Lean project.34- Avoid fake Lean. If a proof is likely hard, mark it as an exercise or use an honest intermediate theorem instead of inventing unsupported code.35- Keep code cells focused. One cell should introduce one definition, API, proof move, or theorem.36- Use comments only where they orient the learner.37- Include expected outcomes in markdown near cells that may require an external Lean kernel.3839## Lean Style4041- Use Lean 4 syntax: `fun x => ...`, `<|` when it improves readability, and no empty lines inside declarations.42- Name examples and lemmas in English when names matter.43- Prefer small proofs with `by`, `simp`, `rw`, `ring`, `omega`, `linarith`, and explicit intermediate lemmas when appropriate.44- Do not hide hard formalization gaps behind `set_option maxHeartbeats`.4546## Bundled Reference4748Read `references/notebook-style.md` for the recommended notebook shape, language modes, Lean cell patterns, and validation checklist.
FrankieeW