lean-interact

You type a sentence of ordinary mathematics into a Claude Code session. A Lean 4 + Mathlib formalization of it appears in a window beside the chat, compiled and checked in about a quarter of a second, together with a short note on which Mathlib lemmas were used and why. When the sentence is false, you get a formal refutation rather than a quietly repaired statement. The knowledge base — a permanent Lean library, an Obsidian vault, a journal — grows as a side effect of the conversation, not as a separate chore.

This is aimed at mathematicians who already know their mathematics and are learning Lean, and whose actual friction is not the proofs but remembering what Mathlib calls things. Finding a name, and verifying that the name exists before it is written into a proof, is a first-class job of the tooling here, not something you are expected to do from memory.

---

A short session

you — let n be an integer, prove that n^4 is congruent to 1 mod 5

assistant — As stated this is false. Take n = 5: 5^4 = 625 = 5 * 125, so n^4 ≡ 0 (mod 5), not 1. The true statement needs the hypothesis that 5 does not divide n; it is Fermat's little theorem at p = 5. I will record both: the refutation of what you wrote, and the corrected theorem. Ambient type ℤ, so [ZMOD 5] (Int.ModEq) rather than [MOD 5] (Nat.ModEq) — subtraction behaves and the counterexample is cleaner.

import NtLean.Preamble

namespace NtLean

/-- The unqualified claim is **false**: `n = 5` is a counterexample, since
$5^4 = 625 = 5 \cdot 125 \equiv 0 \pmod 5$. -/
theorem not_forall_pow_four_modEq_one : ¬ ∀ n : ℤ, n ^ 4 ≡ 1 [ZMOD 5] := by
  intro h
  have h5 := h 5
  -- `Int.ModEq n a b` unfolds to `a % n = b % n`, a decidable equation on closed integers.
  revert h5
  decide

/-- **Fermat's little theorem at the prime 5.**  If `5` does not divide `n`, then
$n^4 \equiv 1 \pmod 5$.  The hypothesis is exactly what
`NtLean.not_forall_pow_four_modEq_one` shows cannot be dropped. -/
theorem pow_four_modEq_one (n : ℤ) (hn : ¬ (5 : ℤ) ∣ n) : n ^ 4 ≡ 1 [ZMOD 5] := by
  -- the case `p = 5`; `norm_num` both discharges `Nat.Prime 5` and reduces `5 - 1` to `4`
  have h := fermat_little_int (p := 5) (by norm_num) n (by exact_mod_cast hn)
  norm_num at h
  exact h

The watcher, in the pane next to the chat, redraws on save:

 OK  Scratch/Current.lean                                    0.2s  14:07:31
 ❝ For every integer n not divisible by 5, n^4 is congruent to 1 mod 5.
   n^4 \equiv 1 \pmod 5 \quad (5 \nmid n)
 ───────────────────────────────────────────────────────────────────────────
 errors 0 · warnings 0 · sorries 0 · decls 2   ▁▃▁▁▂▁  [lsp]  Ctrl-C to quit
 lemmas Int.ModEq, fermat_little_int

assistant — Two lemmas did the work. NtLean.fermat_little_int is our own ℤ-valued form of Fermat's little theorem (Mathlib states it for ZMod p; the cast is the annoying part, so it is done once in NtLean/Congruence.lean and reused). decide closes the refutation because Int.ModEq n a b is by definition a % n = b % n, and on closed integers that is a decidable equation — no arithmetic reasoning needed at all.

One alternative worth knowing: instead of revert h5; decide you could write norm_num [Int.ModEq] at h5. Reach for decide when every number in sight is a literal and the proposition is decidable; reach for norm_num when the goal still contains variables and you want the numerals simplified rather than evaluated.

Both theorems are now in NtLean/Congruence.lean. That promotion, the vault note and the journal entry did not happen during that turn — see Deferred bookkeeping.

---

Requirements

What	Why, and notes
elan	Installs Lean toolchains. lean-toolchain pins leanprover/lean4:v4.28.0; elan reads it and fetches that toolchain on first use.
Mathlib, tag v4.28.0	Pinned in lakefile.toml as git#v4.28.0, deliberately matching the toolchain so lake exe cache get finds prebuilt oleans.
~6 GB free disk	Mathlib's oleans are about 5.4 GB.
git	lake update clones the Mathlib source with it.
Python 3, 3.10 or newer	Standard library only. There is no requirements.txt, no virtualenv, no pip install, nothing vendored. The scripts use modern type syntax, hence 3.10.
bash	All shell scripts are macOS/BSD compatible: no readlink -f, no GNU-only flags.
tmux	Only for tools/session.sh, which lays out the panes. Everything works without it if you start the pieces by hand.
VS Code + leanprover.lean4	For the infoview (goal state under the cursor). Strongly recommended, not required.
Magma	Optional, and remote. See the Magma bridge. The Lean side needs none of it.

Install

The easy path: run /install in a Claude Code session opened on this repository (.claude/skills/install/), and it will walk the steps below, checking each one.

Manually:

# 1. Toolchain. elan reads lean-toolchain and installs Lean v4.28.0 on demand.
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
elan --version

# 2. Dependencies, then the prebuilt Mathlib oleans. Do these in this order.
lake update
lake exe cache get

# 3. The shared import surface. About a minute; everything else imports it.
lake build NtLean.Preamble

# 4. The whole example library, if you want it (optional, a few minutes).
lake build

# 5. VS Code extension + .vscode/ settings (optional).
tools/vscode-setup.sh          # --check to inspect without installing

# 6. The Mathlib name index (optional but this is the point of the repo).
python3 tools/mathlib_index.py build

# 7. Magma bridge (optional).
cp config.example.sh config.sh   # edit, then: source config.sh

The one thing that can go badly wrong. If lake exe cache get reports a miss, stop. A cache miss means the Mathlib revision resolved by lake update does not match a revision the community build farm has published oleans for, and the next lake build will start compiling Mathlib from source — hours of CPU. The tag pin in lakefile.toml exists to prevent exactly this. Check that lean-toolchain says leanprover/lean4:v4.28.0 and that lake-manifest.json still points at Mathlib v4.28.0, fix the mismatch, and re-run lake exe cache get. Never "just let it build".

---

How the interaction goes

This is the part worth reading carefully. The repository is a set of tools, but what it actually is, is a protocol — and the protocol is what makes a turn take seconds rather than minutes.

Starting a session

tools/session.sh                 # --help lists every option

That does four things:

1. Pre-warms Lean. It checks Scratch/Current.lean once through tools/leanserver.py before anything else. Lean runs one language-server worker per open document, so the first check of a file pays the full import load, about 40 s. This is where that cost gets paid — up front, on purpose, so it does not land in the middle of your first thought.
2. Creates a tmux session called lean-interact: the terminal watcher (tools/live.py) on the left, the dashboard server on the right.
3. Serves the browser dashboard on http://127.0.0.1:8765 (--port to change it).
4. Opens VS Code on the project, so the infoview is available.

It is idempotent: an existing lean-interact session is re-used, never killed. Ctrl-b d detaches; tmux attach -t lean-interact comes back.

You now have three views of the same file, all fed by .live/status.json, each answering a different question:

View	Answers
Terminal watcher, tools/live.py	Did the last save compile, and how fast? Header bar, the informal claim, the numbered source with errors inline, counts and a history sparkline.
VS Code infoview, Lean 4 extension	What is the goal state right here? Put the cursor inside a proof and read the hypotheses and the goal after each tactic. Nothing else gives you this.
Browser dashboard, tools/dashboard.py	Where do we stand? The informal claim, the LaTeX, the source, the diagnostics, the sorry list, the lemmas in play, the recent history. The one to put on a second monitor.

One turn, end to end

You state a claim in ordinary mathematical English. Prose, not Lean. "The product of two consecutive integers is even." "Every prime above 3 is 1 or 5 mod 6." "Is 561 a Carmichael number?"

1. Restate. The assistant says back what it understood, with every quantifier, hypothesis and side condition made explicit, and names the ambient type: ℕ, ℤ, or ZMod n. That choice is not cosmetic — truncated subtraction on ℕ silently changes what a statement means, and a ZMod n statement and its Int.ModEq counterpart need different lemmas.
2. At most one question, and only if the answer changes the statement. "Does prime here include 2?" is worth asking. "Would you like me to proceed?" is not. If the reading is unambiguous, no question is asked at all.
3. Search, then verify. Candidate Mathlib names come from tools/mlq.py — by free text, by name fragment, by what the statement says, by namespace, or by an informal concept phrase. Every name that will appear in the proof is then put through tools/leanserver.py verify (or tools/mlq.py --verify), which does not consult the index at all: it asks the compiler and prints the type Lean actually inferred, or MISSING. Verifying 17 names takes about 0.6 s against the warm daemon, so there is no excuse for guessing.
4. Write two files. Scratch/Current.md gets your sentence and its LaTeX — the record of intent, which is what lets anyone later check the Lean against what you asked for. Scratch/Current.lean gets the formal statement and the proof.
5. The watcher recompiles on save. About 0.25 s. All three views update. Note that lakefile.toml sets autoImplicit = false and relaxedAutoImplicit = false: every binder, including type variables, must be declared. A typo'd identifier is a hard error here instead of a silently invented implicit argument — which is exactly what you want when you are reading a statement to check it says what it looks like it says.
6. Iterate to zero. Zero errors and zero sorries. A sorry is a fine intermediate step, and a fine way to show you where the difficulty actually is, but it is never an endpoint, and never left behind without saying so in the first sentence of the reply.
7. Report. The Lean itself (not a description of it), which Mathlib lemmas were used and why each one was the right tool, including the naming logic when it is instructive — Nat.ModEq.add_right reads as "ModEq, adding on the right", and that grammar is how you will find the next lemma without asking. Then exactly one alternative tactic, with the conditions under which you would reach for it instead. One. A survey of five tactics teaches nothing.

Deferred bookkeeping

Promotion into NtLean/, the vault note, the journal bullet, the index rebuild and any commit are deferred. They do not happen inside the turn. They are flushed when you say "record that", or "commit", or "let's stop", or when you change topic.

This is the single most important rule in the protocol, and it was learned the hard way: a turn that also writes documentation takes minutes, and a loop with minute-long turns is not interactive, whatever else it is. Responsiveness wins; the thorough part is deferred, not dropped.

Step-by-step mode

Sometimes you do not want a finished proof to appear. You want to drive it, one tactic at a time, in mathematical language — "induct on n", "split on parity", "use Catalan here" — and see the goal state after each move. That is tools/step.py.

$ tools/step.py init "theorem sq_emod_four (n : ℤ) : n ^ 2 % 4 = 0 ∨ n ^ 2 % 4 = 1"
statement accepted. opening goal:

n : ℤ
⊢ n ^ 2 % 4 = 0 ∨ n ^ 2 % 4 = 1

you — split on the parity of n

$ tools/step.py step "obtain ⟨k, hk⟩ | ⟨k, hk⟩ := Int.even_or_odd n"
ok (0.26s). goal now:

case inl.intro
n k : ℤ
hk : n = k + k
⊢ n ^ 2 % 4 = 0 ∨ n ^ 2 % 4 = 1

case inr.intro
n k : ℤ
hk : n = 2 * k + 1
⊢ n ^ 2 % 4 = 0 ∨ n ^ 2 % 4 = 1

(2 goals open)

you — can omega just do the even branch?

$ tools/step.py step "omega"
tactic failed -- file restored, nothing lost.

  omega could not prove the goal:
  a possible counterexample may satisfy the constraints
  ...

No. omega is a decision procedure for linear integer arithmetic; n ^ 2 is a nonlinear term, so it enters as an opaque atom and nothing constrains it. The fix is to hand omega a linear goal: take the left disjunct, substitute, and rewrite the square into an explicit multiple of 4.

$ tools/step.py step "left"
ok (0.24s). goal now:

case inl.intro
n k : ℤ
hk : n = k + k
⊢ n ^ 2 % 4 = 0

[the odd branch is untouched and still open; elided here]

(2 goals open)

$ tools/step.py step "subst hk"
ok (0.23s). goal now:

case inl.intro
k : ℤ
⊢ (k + k) ^ 2 % 4 = 0
[...]

$ tools/step.py step "have h4 : (k + k) ^ 2 = 4 * (k * k) := by ring"
ok (0.25s). goal now:

case inl.intro
k : ℤ
h4 : (k + k) ^ 2 = 4 * (k * k)
⊢ (k + k) ^ 2 % 4 = 0
[...]

$ tools/step.py step "rw [h4]; omega"
ok (0.24s). goal now:

case inr.intro
n k : ℤ
hk : n = 2 * k + 1
⊢ n ^ 2 % 4 = 0 ∨ n ^ 2 % 4 = 1

The odd branch is the same shape with (2 * k + 1) ^ 2 = 4 * (k * k + k) + 1, and when the last goal closes:

PROOF COMPLETE  (0.24s, 0 errors, 0 sorries)

The mechanics: the proof under construction lives in Scratch/Current.lean and always ends with a cursor (all_goals sorry) holding the remaining goals; step splices a tactic in just above it and re-checks. A failed tactic costs nothing — the file is restored to the state before the attempt and Lean's error is printed. That changes how you use it: trying omega to see whether it happens to work is free, so you try it. undo steps back (history survives across invocations, in .live/step_history/), goal re-prints the current state, show prints the file.

The standing rules

Three rules make the rest work. They are stated absolutely, and CLAUDE.md is their operational form.

• Never assert an unverified Mathlib name. Not in a proof, not in prose, not in a suggestion. Hedging does not help: "I think it might be Nat.ModEq.mul_cancel_left" reads as authoritative the second time it is repeated, costs a compile cycle to disprove, and teaches you something false about a library you are still learning. The same applies to signatures: argument order and hypotheses get checked, never recalled. "I need to look this one up" is always an acceptable answer.
• A false claim gets refuted, formally, not silently repaired. If what you said is wrong, the counterexample is stated and proved as a theorem of its own, and then the corrected statement is proved next to it. not_forall_pow_four_modEq_one and not_forall_sq_emod_eight in NtLean/Congruence.lean exist for that reason. The refutation is a permanent record of the boundary of the true statement, which is worth more than the repair.
• Generalize upward, keep the specialization as a corollary. If the proof never used primality, say so and state it without primality. NtLean/Chebyshev.lean is the extreme case: everything there is proved over an arbitrary CommRing, and the ℤ statements are one-line consequences.

There is also a mechanical guard, tools/check_names.py, which enforces the first rule across the whole repository rather than one turn at a time. Every Mathlib-looking name cited anywhere in NtLean/, vault/ or book/ must either exist in Mathlib or carry the marker (absent at Mathlib v4.28.0) on its own line, so a reader meets the warning at the point of use. It also flags broken [[wikilinks]] in the vault. It exits non-zero otherwise; run it before committing documentation and after any Mathlib bump.

The skills

.claude/skills/ holds the procedures, invoked by name or automatically when the request matches.

Skill	What it drives
formalize	The main loop above: restate, search, verify, write, iterate to zero, report, defer the bookkeeping.
formalize-from-magma	Start from Magma source or a computational experiment: run it, extract the mathematical claim it encodes, sweep parameters to separate accident from theorem, then hand the claim to formalize.
mathlib-lookup	Find and verify a name and report its real elaborated type — from the naming grammar, then tools/mlq.py, then exact? / apply? / rw? / hint.
lean-session	Bring up, check or repair the live session: the watcher, the dashboard, the infoview, a stale .live/status.json, a port already in use, an olean cache that is not in place.

---

What is in the box

Path	What lives there
Scratch/Current.lean	The live Lean file. Recompiled on every save. Disposable by design.
Scratch/Current.md	Its sidecar: the informal sentence and its LaTeX. The record of intent.
NtLean/	The permanent library. Results are promoted here once they compile with no sorry.
NtLean/Preamble.lean	The shared import surface. Every file here imports this, never Mathlib.
NtLean.lean	Root module; aggregates the chapters.
tools/	All executable tooling. Python 3 stdlib and bash only.
vault/	Obsidian knowledge base: one note per result, plus tactic, naming and style notes, densely wikilinked. vault/Formalization Style.md is the canonical record of how Lean is written here.
book/	Jupyter Book: the linear, readable narrative built out of the vault and the library.
magma/	Magma sources (.m), run remotely, used to compute the examples that motivate a formalization.
.live/	All transient state: status.json, compile_log.jsonl, mathlib.db, the daemon socket, step_history/. Gitignored.
CLAUDE.md	The operating manual for the assistant working in this repository.
MEMORY.md	Durable preferences and facts, with an append-only "Preferences learned" section.
PLAN.md, JOURNAL.md	Forward-looking plan; reverse-chronological record of what changed and why.
lakefile.toml, lean-toolchain, lake-manifest.json	The pins. All three committed; the manifest is what makes the Mathlib revision reproducible.

Every script in tools/ is executable, carries a one-line usage comment at the top, and has a --help that is the authority on its flags — not this table.

Tool	For	Example
tools/session.sh	Bring up the whole workspace and pre-warm Lean.	tools/session.sh --port 8765
tools/live.py	The terminal watcher; writes .live/status.json.	tools/live.py --once --plain
tools/dashboard.py	The browser view over .live/status.json.	tools/dashboard.py --open
tools/leanserver.py	The warm LSP daemon, and direct access to it.	tools/leanserver.py verify Nat.ModEq.symm Nat.Prime.two_le
tools/leanlib.py	Shared Lean runner; also a CLI for one file. --status gives a one-line report (~80 bytes); the default JSON embeds the whole source (~26 kB).	python3 tools/leanlib.py Scratch/Current.lean --status
tools/mlq.py (or tools/mlq)	Mathlib name search, and the anti-hallucination --verify.	tools/mlq --about "chinese remainder"
tools/mathlib_index.py	Build or inspect the SQLite FTS index of Mathlib.	python3 tools/mathlib_index.py build
tools/step.py	One tactic at a time, with the goal state after each: init, step, goal, undo, show.	tools/step.py step "omega"
tools/check_names.py	The standing invariant, repo-wide. Exits non-zero on a defect.	python3 tools/check_names.py --fast
tools/vscode-setup.sh	Install the Lean 4 extension, write .vscode/.	tools/vscode-setup.sh --check
tools/magma_run.sh	Optional: run Magma on the configured host, clean output.	tools/magma_run.sh -e 'print CRT([2,3],[3,5]);'
tools/magma_check.py	Heuristic Magma linter. Needs no Magma.	python3 tools/magma_check.py magma/nt_basic.m

Searching Mathlib

Four ways to ask, one way to check the answer:

tools/mlq symm modeq                            # free text, all terms must match
tools/mlq --name Nat.ModEq                      # by name substring or prefix
tools/mlq --about "chinese remainder"           # over statements and docstrings
tools/mlq --concept "order of an element mod n" # an informal phrase
tools/mlq --namespace Nat.Prime --kind theorem  # restrict the search

tools/mlq --verify Nat.ModEq.symm Nat.Prime.two_le

The search side is a text scan of Mathlib's sources indexed into SQLite: about 239,000 declarations, built in roughly 10 s. It can be out of date, and it cannot see names produced by macros. --verify cannot be out of date, because it does not look at the index — it elaborates #check @NAME and reports the type Lean inferred. All names go into one snippet, so verifying forty costs what verifying one costs. --verify alone checks against NtLean.Preamble through the warm daemon (about 0.3 s, and a name outside the preamble's imports reports as a false MISSING); adding --verify-full checks against the whole of Mathlib in a separate process — a couple of minutes, authoritative, and it does not evict the warm daemon. Use the full check before writing a name into the vault. --verify takes a variable number of names, so put it last:

tools/mlq --verify-full --verify Nat.ModEq.symm     # not: --verify NAME --verify-full

The Magma bridge

Entirely optional, and it does not exist unless you configure it. Magma is commercial and usually lives on a departmental server rather than a laptop, so this repository drives it over SSH.

cp config.example.sh config.sh
# set LEAN_MAGMA_HOST (reachable with passwordless ssh) and LEAN_MAGMA_BIN
source config.sh
tools/magma_run.sh -e 'print CRT([2,3,2],[3,5,7]);'

config.sh is gitignored. With nothing configured, tools/magma_run.sh prints an actionable message rather than failing obscurely. It handles the two things that break naive invocations: the binary is usually on the PATH of a login shell only, and Magma prints a banner ending in a row of asterisks and a session-log path that has to be stripped before the real output. The intended use is to compute a table — orders, residue counts, Legendre symbols, small-case searches — decide from it what the general statement is, and keep the cleaned output in the vault note as the evidence behind the theorem. NtLean contains several results that arrived this way, and one non-result: the widened sweep that found {n^2 mod 8} = {0, 1, 4} and killed the over-generalization before it was formalized.

---

Why it is fast

Three measurements on the machine this was built on (16 GB RAM, 5.4 GB of Mathlib oleans). They are the whole design rationale:

	Cost per check
import Mathlib, one-shot lake env lean	~111 s
import NtLean.Preamble, one-shot	~24 s
import NtLean.Preamble, warm LSP daemon	~0.25 s

The first number is why NtLean/Preamble.lean exists: all of Mathlib will not stay in the page cache, so every one-shot check re-reads gigabytes from disk. No working file says import Mathlib; they all import the preamble, one shared module holding the elementary-number-theory slice. If you need a module the preamble lacks, add it there and rebuild the preamble — do not widen the import in a working file. The one deliberate exception is mlq.py --verify-full, which must import all of Mathlib precisely because it has to see names nobody has imported yet.

The third number is why tools/leanserver.py exists. It keeps a single lake env lean --server process alive with the environment already elaborated and pushes each edit as an LSP didChange, so only the changed file is re-elaborated and the imports stay in memory. Everything falls back to one-shot lake env lean if the daemon is down, so nothing hard-depends on it; the watcher's footer shows [lsp] or [oneshot], and a silent fallback is the usual reason the loop suddenly feels slow.

One cost you cannot avoid: Lean runs one worker per open document, so the first check of any given file pays the import load, about 40 s, once. tools/session.sh warms Scratch/Current.lean at startup for exactly this reason.

The inner loop never builds. It elaborates a single file against Mathlib's already-built oleans. lake build is reserved for the moment a result is promoted into NtLean/ and genuinely has to become part of the library.

---

The example library

NtLean/ is 134 theorems, no sorries, all building. It is the demonstration material: what the loop above actually produced.

Module	Contents
Basic	Parity, elementary divisibility, Nat.gcd warm-ups, Euclid's step gcd m n = gcd (n % m) m.
Congruence	The Nat.ModEq API worked through; cancellation under coprimality; Euler and Fermat over both ℕ and ℤ; the Chinese Remainder Theorem; the Carmichael number 561 (561 = 3 * 11 * 17, not prime, and 2^560 ≡ 1 [MOD 561]); squares mod 4 in all four forms, including the false mod-8 analogue; the n^4 mod 5 pair from the demo above.
Divisibility	Bézout in both directions, coprimality, Euclid's lemma, and the classical digit tests: divisibility by 3 and by 9 from the digit sum, by 11 from the alternating sum — plus the proof that the same trick fails for 7.
Primes	Primality basics, infinitude of the primes (twice: exists_prime_ge and Set.Infinite), concrete factorizations (91, 2047, the Mersenne factor 2^11 - 1 = 23 * 89), quadratic residues mod 7, and Wilson's theorem with its converse — prime_iff_wilson_int, including the n ≠ 1 side condition and the theorem showing it cannot be dropped.
Fibonacci	gcd(F_m, F_n) = F_gcd(m,n), both cited from Mathlib and proved independently by Euclidean descent (fib_gcd_from_scratch); the divisibility criterion F_m ∣ F_n ↔ m ∣ n for m ≥ 3; and the elliptic (Ward/Somos) identity F(4n+2)F(2)^3 - F(2n+4)F(2n)^3 + F(2n+2)^3 F(2n-2) = 0 over ℤ, which turns out to be Catalan's identity multiplied by F(4n+2).
Chebyshev	The deepest development here. See below.

NtLean/Chebyshev.lean is worth a look on its own. Mathlib defines T_n by the recurrence and proves the composition law by induction. This module instead defines it geometrically: work over a commutative ring K with an element i satisfying i^2 = -1, take the conic c^2 + s^2 = 1 presented as AdjoinRoot (Y^2 - (1 - c^2)) over K[c], put z = c + i*s, and read off

z ^ n = T_n(c) + i * s * U_n(c)

as the definition of T_n. Then T_n ∘ T_m = T_{nm} is just (z^m)^n = z^(mn) with components compared — which is legitimate exactly because the quotient is free of rank 2 over K[c] with basis {1, s} (repr_unique, the crux of the whole argument). The module proves that uniqueness, the composition law over any CommRing (cheb_comp, cheb_comp_of_comm_ring, and the ℤ specialization as a corollary), the product formula 2 T_m T_n = T_{m+n} + T_{|m-n|} (two_T_mul_abs), the Pell relation, coprimality of T_n and U_n, and U as a strong divisibility sequence (U_isGCD). Nothing anywhere in it needs K to be a domain, or nontrivial, or of characteristic zero. That is the "generalize upward" rule taken as far as it goes.

---

Status

This is a working research instrument, not a product. It was built for one person's actual day-to-day formalization work and then generalized; it is published because the loop turned out to be useful, not because it is finished.

What is guaranteed: the 134 theorems in NtLean/ build against Lean v4.28.0 and Mathlib v4.28.0, with no sorry and no unverified name; the Python is standard library only and will not rot when a dependency bumps; the shell is macOS/BSD compatible.

What is not: any API stability at all. .live/status.json is at schema 1 and its exact shape is documented at the top of tools/leanlib.py, but it will change when the views need it to. The tools were developed and measured on macOS; nothing in them should be Linux-hostile, but nothing has been tested there either. The Magma bridge is optional and depends entirely on a host you supply. Timings are measurements from one machine, not promises. Pinning to a newer Mathlib is expected to break proofs — that is the normal cost of a fast-moving library, and tools/check_names.py exists to tell you exactly where.

Issues and pull requests welcome at https://github.com/YOUR-GITHUB-USER/lean-interact.

License

MIT. See LICENSE.