nasqret

nasqret/lean-interact

Settings file Claude Code

Agent settings declaring 56 allowed tools.

nasqret/lean-interact

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…

nasqret/lean-interact

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…

nasqret/lean-interact

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…

nasqret/lean-interact

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…

nasqret/lean-interact

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…

nasqret/lean-interact

Instructions file

Instructions for nasqret/lean-interact, covering claude.md — operating instructions for this repository, 0. start of every session, 1. the formalization loop, turn length, and deferred bookkeeping and when the proof is the interesting part.