Interactive Lean 4 + Mathlib formalization from a Claude Code conversation
Skill Claude CodeCodex
Turn Magma code into a formalized Lean theorem. Use whenever the user pastes or points at Magma source, asks what a Magma routine is really proving, asks to formalize a computation or a computationally-discovered pattern, or wants a Magma experiment turned into a general statement. Covers running the code on…
Skill Claude CodeCodex
Formalize a claim of ordinary mathematics as Lean 4 + Mathlib and drive the live compile loop to zero errors. Use whenever the user states a mathematical claim, conjecture, exercise or definition; asks to formalize, state, prove, check or Lean-ify something; corrects or refines a previous formalization; asks why a…
Skill Claude CodeCodex
Install and bootstrap the lean-interact harness on a fresh machine, from a Claude Code session inside a clone of this repository. Use when the user says install, set up, bootstrap, get started, first run, new machine, fresh clone, or make this work; when the user asks what they need to have installed; when any tool…
Skill Claude CodeCodex
Bring up, check, or repair the live Lean session: the terminal watcher over Scratch/Current.lean, the browser dashboard, and the VS Code infoview. Use when the user says start a session, open the windows, show me the live view, is the watcher running, restart the dashboard, nothing is updating, or when a formalization…
Skill Claude CodeCodex
Find and verify the name of a Mathlib lemma, theorem, definition, instance or tactic, and report its real elaborated type. Use whenever the user asks what a theorem is called, whether Mathlib has some fact, what the exact statement or hypotheses of a lemma are, or what the API of a type or namespace looks like; and…