Skip to content

PLAN.md

Latest commit

 

History

History
157 lines (129 loc) · 9.23 KB

PLAN.md

File metadata and controls

157 lines (129 loc) · 9.23 KB
Raw

PLAN

This is a starting point, not a specification. It ships as a suggested roadmap through elementary number theory, because a blank plan file is harder to edit than a wrong one. Cross out what does not interest you, reorder freely, and replace the whole thing once you know what you actually want to formalize. The point of the harness is that a good question can be formalized the moment it comes up, not that these phases get completed in order.

Check items off as they land, and record the landing in JOURNAL.md.

What already exists. The NtLean/ library ships with 134 theorems, zero sorries, all building — worked examples covering a good part of Phases 1 and 2 below, plus material well past them. They are demonstration material: read them to see the house style, or delete them and start clean. Pointers are given under each phase.

  • NtLean/Basic.lean — conventions, parity, elementary divisibility, gcd warm-ups
  • NtLean/Congruence.lean — the Nat.ModEq API, worked congruence computations, CRT
  • NtLean/Divisibility.lean — Bezout, coprimality, Euclid's lemma
  • NtLean/Primes.lean — primality basics, infinitude of primes, concrete primes
  • NtLean/Fibonacci.lean — Fibonacci as a strong divisibility sequence
  • NtLean/Chebyshev.lean — Chebyshev polynomials from the conic c^2 + s^2 = 1

Last reviewed: template as shipped.

Phase 0 — Get the loop running

The harness itself is built; this phase is what you do once, after cloning.

  • elan installed, and lean-toolchain honoured (Lean v4.28.0).
  • lake exe cache get — prebuilt Mathlib oleans in place. Mathlib is pinned to the git tag v4.28.0 to match the toolchain precisely so that this works. If it misses, fix the pin; do not start a source build.
  • lake build NtLean.Preamble — the focused import surface every working file uses.
  • python3 tools/mathlib_index.py build — the searchable index of Mathlib declarations (~239,000 of them, built from source in ~10 s).
  • tools/session.sh — brings up the live views and pre-warms the language-server daemon. Confirm that a save of Scratch/Current.lean is answered in about a quarter of a second rather than tens of them.
  • python3 tools/check_names.py — the standing invariant, green on a fresh clone.
  • Fill in the template sections of MEMORY.md. Do this before the first real request; it is what the assistant calibrates on.
  • Optional, and only if you have access to it: copy config.example.sh to config.sh and set LEAN_MAGMA_HOST and LEAN_MAGMA_BIN for the computer-algebra bridge. The Lean side needs none of it.
  • End-to-end smoke test: state a sentence of ordinary mathematics, watch a theorem come out of it, promote it into NtLean/, write the vault note and the journal bullet.

Phase 1 — Elementary congruences, as proof of concept

The goal here is not mathematical depth. It is to prove the loop works and to build the reflexes: search before you recall, verify before you write, restate before you formalize.

  • Reflexivity, symmetry and transitivity of Nat.ModEq / Int.ModEq, restated in your own words and proved from Mathlib rather than quoted.
  • Compatibility of congruence with addition and multiplication.
  • Cancellation: when may a common factor be cancelled, and what exactly is the coprimality hypothesis Mathlib asks for.
  • Divisibility rules (by 3, by 9, by 11) as worked examples of "ordinary sentence in, formal statement out".
  • A vault note per result, each naming the lemmas used and one alternative tactic.
  • Settle ℕ vs ℤ vs ZMod n: which you state things in by default and how you move between them. Record the answer in vault/Formalization Style.md, which ships with a provisional answer marked as such.

Already in the library: the Nat.ModEq API, cancellation under coprimality, the divisibility rules by 3, 9 and 11, and squares mod 4 — see NtLean/Congruence.lean and NtLean/Divisibility.lean.

Phase 2 — CRT, orders, Fermat and Euler

  • Chinese Remainder Theorem: locate Mathlib's form or forms (verify before use) and state the classical two-congruence version you actually want to quote.
  • Solving explicit simultaneous congruences, with the construction and not only existence.
  • Multiplicative order mod n: the order of an element of (ZMod n)ˣ, its basic properties, and the fact that it divides the group order.
  • Fermat's little theorem and Euler's theorem in the classical congruence form, not only the group-theoretic form.
  • Euler's totient: values, multiplicativity, and the formula on prime powers.
  • Primitive roots mod p: existence, and how Mathlib packages cyclicity.

Already in the library: Euler and Fermat over both ℕ and ℤ, Wilson's theorem together with its converse, CRT existence with a worked instance, and the Carmichael number 561 — see NtLean/Congruence.lean and NtLean/Primes.lean.

Phase 3 — Quadratic residues and reciprocity

  • Legendre symbol: Mathlib's definition, and the bridge to "is a nonzero square mod p".
  • Euler's criterion.
  • Quadratic reciprocity and both supplementary laws.
  • Deciding solvability of a given x^2 ≡ a (mod p) by hand-style computation, formalized.
  • Counting quadratic residues mod p, and mod prime powers.

Phase 4 — Computation feeding formalization

This phase presumes the optional Magma bridge. Nothing above depends on it, and the same shape of work can be done with any computational tool you can drive from a shell.

  • A stable pattern: run the computation, capture the cleaned output, keep it in the vault note as the evidence that motivated the statement.
  • Scripts under magma/ for the recurring computations: order tables, residue tables, Legendre symbol tables, small-modulus searches for counterexamples.
  • Computation as conjecture generator: search small cases, find the pattern, then formalize the general claim in Lean.
  • Computation as sanity check before formalizing: if the claim already fails at n = 12, find that out in two seconds rather than in an hour of failed proof.
  • Decide and document how computed output is quoted in book/.

Already in the library: the shipped examples include results that came out of exactly this loop — squares mod 4 (with the mod-8 analogue refuted), and the Chebyshev gcd law, where the computation showed that the obvious guess about T is false and that U is the sequence with the strong divisibility property.

Open questions

Genuinely undecided as far as this template is concerned. Do not guess an answer into the documentation: decide, then record the decision. Some of these ship with a provisional answer in vault/Formalization Style.md, clearly marked as provisional and safe to overrule.

  • Default type for statements. ℕ, ℤ, or ZMod n? Each makes a different set of lemmas reachable, and mixing them costs coercion pain. Usually resolved during Phase 1.
  • How much of a proof should be decide or omega. Both are fast and honest, but they teach nothing about Mathlib and do not generalize. Where is the line?
  • Naming in NtLean/. Follow Mathlib's naming grammar exactly, or use names that read like your own prose? Consistency with Mathlib helps discovery; your own names help reading.
  • Granularity of NtLean/ modules. One module per topic, or one per session? Only a real question once there are more than a handful of results.
  • Vault-to-book pipeline. Whether book/ chapters are generated from vault notes or written separately. Generation is tempting but couples the two layers permanently.
  • How much of the failed attempts to keep. Failed proof attempts are where the learning is, but they bloat both the vault and the journal.

Deliberately out of scope

Stated so the project does not quietly become something else. This is the shipped opinion; change it if your project is a different project.

  • Analytic number theory. No Dirichlet series, no prime number theorem, no character sums beyond what quadratic reciprocity needs. The domain is elementary number theory.
  • Algebraic number theory. No number fields, no ideal class groups, no elliptic curves.
  • Contributing to Mathlib. This project consumes Mathlib and does not upstream. If something is genuinely missing, that is a note in the vault, not a pull request.
  • Building Mathlib from source. The matched pin exists precisely so that the olean cache is usable. If the cache ever misses, fix the pin; do not start a multi-hour build.
  • A general-purpose Lean IDE. The harness serves one workflow. No plugin system, no configuration surface beyond --help flags.
  • Third-party Python dependencies. Standard library only, permanently. See MEMORY.md.
  • Automated proof search at scale. exact? and friends used interactively are fine; a background prover farm is not the point.
  • Teaching the mathematics. The teaching contract in CLAUDE.md is about Lean and Mathlib. If you want the mathematics explained too, say so in MEMORY.md — but say it, because the default assumes you already know it.