From 9a491aa62f9937afa863344334e0d01f1cf3bb5f Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Sat, 5 Sep 2026 21:15:37 -0400 Subject: [PATCH] docs: presentation & navigation for newcomers (Phase 4) - README: add CI status badges (proof-lean, proof-verify, telperion-lean-e2e) and a scannable TL;DR that routes a first-time visitor to STATUS.md (proven-vs-open), the verify section, and Telperion getting-started. - telperion/docs/GETTING_STARTED.md (new): install -> generate -> and, crucially, VERIFY the emitted Lean locally end-to-end (pinned leanprover/lean4:v4.32.0 + 'lake exe cache get' Mathlib cache + 'lake build') -- the audit's #1 doc gap. - telperion/docs/ARCHITECTURE.md (new): the untrusted-generator/trusted-kernel model, the certify->validate->emit->freeze pipeline, the emitter catalog, the self-verification layer, and the enforced engine vs bg/ research-lab boundary. - telperion/CONTRIBUTING.md (new): how to add a certificate shape, incl. the mandatory emitter-sensitivity stance, the manifest entry, and the CI gates. - telperion/README.md: a 'New to Telperion?' pointer to the three docs above. No code or mathematics changed. All internal links verified to resolve. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01W4CnMPKEstq3yVjTgjtreY --- README.md | 15 ++++ telperion/CONTRIBUTING.md | 99 ++++++++++++++++++++++++ telperion/README.md | 5 ++ telperion/docs/ARCHITECTURE.md | 108 ++++++++++++++++++++++++++ telperion/docs/GETTING_STARTED.md | 122 ++++++++++++++++++++++++++++++ 5 files changed, 349 insertions(+) create mode 100644 telperion/CONTRIBUTING.md create mode 100644 telperion/docs/ARCHITECTURE.md create mode 100644 telperion/docs/GETTING_STARTED.md diff --git a/README.md b/README.md index 066e5beb..78567be8 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,20 @@ # Arda +[![proof-lean](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-lean.yml/badge.svg)](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-lean.yml) +[![proof-verify](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-verify.yml/badge.svg)](https://github.com/DrMurphyIsIn/Arda/actions/workflows/proof-verify.yml) +[![telperion-lean-e2e](https://github.com/DrMurphyIsIn/Arda/actions/workflows/telperion-lean-e2e.yml/badge.svg)](https://github.com/DrMurphyIsIn/Arda/actions/workflows/telperion-lean-e2e.yml) + +> **TL;DR** — A Lean 4 / Mathlib formalization of the machine-checkable core of a +> 42-year-old extremal-graph-theory problem (the Brualdi–Goldwasser tree maximizer, +> `per(L(T))/∏deg`), the reusable certificate engine — [**Telperion**](telperion/) — +> that generated it, and a second front in proof complexity. Everything is checked +> by the Lean kernel with **no `sorry`, no added axioms**, and an *executable* honesty +> ledger. **The conjecture is not claimed proved.** New here? Start at +> **[STATUS.md](STATUS.md)** for the proven-vs-open map, then see +> [Verifying the claims](#verifying-the-claims) to re-run the kernel checks yourself. +> Want to use the engine on your own problem? See +> [`telperion/docs/GETTING_STARTED.md`](telperion/docs/GETTING_STARTED.md). + This repository is a working research program, kept honest in public form: machine-checked progress on a 42-year-old open problem in extremal graph theory, the general-purpose proof engine that campaign forged, and — most diff --git a/telperion/CONTRIBUTING.md b/telperion/CONTRIBUTING.md new file mode 100644 index 00000000..4ce9df2a --- /dev/null +++ b/telperion/CONTRIBUTING.md @@ -0,0 +1,99 @@ +# Contributing to Telperion + +Telperion is an **untrusted generator over a trusted kernel**: contributions may +be as clever or as hacky as you like internally, because the Lean kernel re-checks +the output. What the review process protects is not the generator's cleverness but +its **honesty** — that every emitted theorem is non-vacuous, byte-reproducible, and +means what it says. This guide is about clearing those gates. + +New here? Read [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) first (the pipeline +and the engine/research-lab boundary), then [`docs/GETTING_STARTED.md`](docs/GETTING_STARTED.md). + +## Setup + +```bash +pip install -e "telperion[dev]" # sympy + pytest + numpy + networkx +cd telperion +python -m pytest tests -q # the suite should be green before you start +``` + +Keep the **engine core (`src/telperion/`) sympy-only**. numpy/networkx belong to +the `bg/` research lab and the `[bg]` extra; cvxpy belongs to the `[sdp]` finders. +`tests/test_core_boundary.py` enforces this and will fail if the core imports them. + +## Adding a certificate shape (an emitter) + +1. **Write the emitter** — a new `src/telperion/emit_.py` whose class + subclasses `Emitter` (in `workflow.py`) and implements + `emit_body(family, profile) → (text, n_theorems)`. Certify in **exact + arithmetic** (`fractions.Fraction` / sympy); no floats on the certificate path. +2. **Register it** — add the import to `src/telperion/__init__.py` (in the right + tier group). If it introduces a new certificate *kind*, register that kind in + `certify.py`. +3. **Declare a sensitivity stance** — add an entry to the `REGISTRY` in + `src/telperion/emitter_sensitivity.py`. This is mandatory: + `tests/test_certificate_sensitivity.py::test_every_emitter_is_classified` + fails until you do. Choose honestly: + - **`CERTIFICATE_SENSITIVE`** — the emitted theorem carries a corruptible + witness (a specific numeric/algebraic identity). You must also add a + negative-control adapter under `negctrl_adapters/` that forges the witness + and confirms the kernel rejects it. + - **`STRUCTURALLY_NONVACUOUS`** — the theorem is positivity / decidability / + finite-cover / hypothesis-gated glue with no corruptible witness; the + built-in structural non-vacuity check suffices. Write a one-line note saying + *why* (see the existing entries — e.g. `HalfPlaneDiskEmitter` — as a model). +4. **Add a worked example** — a `examples//generate.py` that certifies → + emits → writes `lean/.lean`, and supports `--check` (drift/byte-stability). + Include a `lakefile.toml` + `lean-toolchain` pinned to `leanprover/lean4:v4.32.0`, + matching every other example. +5. **List it in the manifest** — add a `[[check]]` block to `telperion.toml` + (`name`, `script`, `group`). An unlisted `generate.py` is a hard CI failure + (the manifest-completeness gate). Pick the group by regeneration cost: + `quick` (seconds), `heavy` (minutes), `audit` (adversarial/large), `sdp` + (needs cvxpy). + +## Before you open a PR + +Run what CI runs: + +```bash +cd telperion +python -m pytest tests -q # unit tests (incl. the sensitivity gate) +PYTHONPATH=src python -m telperion.cli verify --group quick # regen drift + byte-stability +python examples//generate.py --check # your example is byte-stable +``` + +And **verify the emitted Lean actually compiles** — the whole point: + +```bash +cd examples//lean && lake exe cache get && lake build +``` + +If you cannot run Lean locally, the CI `telperion-lean-e2e` job compiles emitted +Lean for you; do not merge on a red Lean job. + +## CI gates your PR must pass + +| Workflow | What it checks | +|---|---| +| `telperion-test` | pytest across sympy versions + `verify --group quick` (drift + byte-stability). | +| `telperion-lean-e2e` | regenerate emitted Lean and `lake build` it against pinned Mathlib. | +| `telperion-casestudy` / `telperion-audit` | `verify --group heavy` / `--group audit` re-certification. | +| `telperion-production` | frozen-artifact compile + regeneration diff. | +| `telperion-comparator` | independent second check (whitelisted axioms only). | + +## House rules + +- **Honesty flags are load-bearing.** Keep `conjecture1_proved = False`; label + ranges, open pieces, and negative results as such. Preserve failed-route + `*_nogo*` modules with their reasons — they are part of the record. +- **No floats on the certificate path.** Exact arithmetic only. +- **Don't hand-edit emitted `.lean` files.** They are regenerated; edit the + generator and re-run. + +## Licensing + +The Telperion engine (`src/`, CLI, MCP server) is **BUSL-1.1**; emitted +certificates and the `examples/` artifacts are Apache-2.0 (they are yours). See +[`../LICENSING.md`](../LICENSING.md). By contributing you agree your changes are +licensed on the same split terms. diff --git a/telperion/README.md b/telperion/README.md index 161cdebc..6db1a5a3 100644 --- a/telperion/README.md +++ b/telperion/README.md @@ -4,6 +4,11 @@ claims into kernel-checked Mathlib proofs by exact-arithmetic witness, not by trust.** +> **New to Telperion?** → [Getting Started](docs/GETTING_STARTED.md) (install → +> generate → verify a proof locally) · [Architecture](docs/ARCHITECTURE.md) (how it +> works; engine vs. research lab) · [Contributing](CONTRIBUTING.md) (add a +> certificate shape). + You describe your problem as a parameterized *family* of statements. Telperion certifies each instance in exact rational arithmetic, then emits Lean 4 that Mathlib's kernel re-proves from scratch. **The generator is untrusted by diff --git a/telperion/docs/ARCHITECTURE.md b/telperion/docs/ARCHITECTURE.md new file mode 100644 index 00000000..a482cabb --- /dev/null +++ b/telperion/docs/ARCHITECTURE.md @@ -0,0 +1,108 @@ +# Telperion architecture + +Telperion is a **certificate generator with an untrusted-generator / trusted-kernel +trust model**: it may use any heuristic, search, or SDP solver to *find* a +certificate, but the output is Lean that Mathlib's kernel re-proves from scratch. +Nothing Telperion does needs to be trusted — a wrong certificate is a compile +error, never a false theorem. This document maps the code onto that model. + +## The one boundary that matters: engine vs. research lab + +The package has two clearly separated parts, and the separation is **enforced by +a test** (`tests/test_core_boundary.py`), not just convention: + +| | Path | What it is | Depends on | +|---|---|---|---| +| **Engine** | `src/telperion/` (everything except `bg/`) | The reusable, problem-agnostic tool: the pipeline, ~78 certificate emitters, the CLI, the MCP server, the self-verification layer. | sympy only (core) | +| **Research lab** | `src/telperion/bg/` | The Brualdi–Goldwasser–specific research code (spectral helpers, tree search / MAP-Elites, Ehrhart probes). *Not* part of the reusable engine. | `[bg]` extra (numpy, networkx) | + +The core engine never imports `bg/`. If you want to use Telperion on your own +problem, you only ever touch the engine; the `bg/` lab is one large worked +example that happens to live in the same repository. + +## The pipeline + +Every emitted file goes through the same four stages: + +``` +define ─▶ certify() ─▶ validate ─▶ emit() ─▶ lake build (Lean kernel) ─▶ freeze() + family exact cert sanity Lean re-proves byte-stable + spec per instance gates output from scratch artifact +``` + +- **`family.py`** — an `InequalityFamily` is a parameterized grid of instances + (name, symbols, grid axes, constants, and the target per grid point). This is + the only thing *you* write. +- **`certify.py`** — certifies each instance in **exact `fractions.Fraction` / + sympy** arithmetic. No floats on the certificate path. +- **`workflow.py`** — `emit()` renders the certified family to Lean. All emitters + subclass the single `Emitter` base class here (interface: `emit_body(family, + profile) → (text, n_theorems)`); `LeanProfile` (in `lean.py`) carries + everything about the target Lean project the output must respect. +- **`provenance.py`** — stamps the input-hash header, and `freeze()` writes the + byte-stable artifact + manifest that the regeneration-diff gate compares against. +- **`lean.py`** — the Lean rendering (`file_shell`, the tactic skeletons; the + tactic contract is documented in [`TACTIC_CONTRACT.md`](TACTIC_CONTRACT.md)). + +## The certificate emitters + +~78 `emit_*.py` modules, each producing one *shape* of certificate. They are +discovered by explicit imports in `src/telperion/__init__.py` (grouped by tier), +and every family generator is listed in the top-level `telperion.toml` manifest +(the source of truth for what CI regenerates and checks). Broadly: + +- **General / textbook** — direct Pólya positivity, SOS (rational, Artin + denominators), the Positivstellensatz family (Handelman, Putinar, + Nullstellensatz + infeasibility/refutation), Chvátal–Gomory rounding, Sturm, + Bernstein, exact identities, p-adic valuations, brackets, finite case analysis. +- **Analytic / RH** — zero-free-region atoms, half-plane–disk (Borel–Carathéodory), + Jensen zero-count, transcendental enclosures. +- **Brualdi–Goldwasser** — tight-cap enclosure, affine-parameter endpoint, + recursion/cavity closure, per-size dominance, curvature-boundary, integrality + gate (23-adic), and more. +- **Proof complexity** — SOS refutation, pseudo-expectation duality, XOR moment + PSD, cone/Farkas infeasibility. + +Under the positivity shapes sits an **automatic certificate search** (the Pólya +engine plus optional SDP finders under the `[sdp]` extra), so for many statements +you never construct the certificate by hand. + +## The self-verification layer + +The Lean kernel catches *false* theorems. It cannot catch a theorem that is +true-but-**vacuous** (e.g. a reflexive `X = X` that proves nothing). Telperion +adds a layer specifically for that gap: + +- **`nonvacuity.py`** — refuses reflexive/trivial statements at emit time + (structural), and, for `CERTIFICATE_SENSITIVE` emitters, checks that corrupting + the certificate actually breaks the claim (semantic). +- **`emitter_sensitivity.py`** — a registry forcing every emitter to declare a + stance: `CERTIFICATE_SENSITIVE` (carries a corruptible witness → needs a + kernel-gated negative-control adapter) or `STRUCTURALLY_NONVACUOUS` + (positivity / decidable / hypothesis-gated glue → no adapter needed). A new + emitter that declares neither **fails the test suite** until it does. +- **`negctrl_adapters/`** — the per-emitter negative controls: forge the + certificate, confirm the kernel rejects the forgery. +- **`comparator.py`** — the independent second check (whitelisted axioms only); + see [`COMPARATOR.md`](COMPARATOR.md). +- **`circularity.py`, `coverage.py`, `faithfulness.py`, `metacircular.py`** — + non-circularity witnesses, coverage profiling, seeded-exact-point faithfulness, + and the audit calculus pointed at itself (which documents the one irreducible + trusted floor: whether a formal statement *means* the informal claim is + undecidable — Löb/Gödel). + +## Interfaces + +- **CLI** (`cli.py`, console script `telperion`) — `certify`, `emit`, `diff`, + `verify --group `, `prove`, and the diagnosis helpers. +- **MCP server** (`mcp_server.py`, console script `telperion-mcp`, `[mcp]` extra) + — exposes the same certify→emit pipeline as ~15 tools to LLM/RL agents, with no + emit-without-certify path. Registered as a Claude plugin under + `claude-plugin/`. + +## Where to look next + +- Use it end-to-end: [`GETTING_STARTED.md`](GETTING_STARTED.md). +- Add a new certificate shape: [`../CONTRIBUTING.md`](../CONTRIBUTING.md). +- The trust model in prose: [`METHODOLOGY.md`](METHODOLOGY.md). +- The exact Mathlib tactic bindings: [`TACTIC_CONTRACT.md`](TACTIC_CONTRACT.md). diff --git a/telperion/docs/GETTING_STARTED.md b/telperion/docs/GETTING_STARTED.md new file mode 100644 index 00000000..314410ec --- /dev/null +++ b/telperion/docs/GETTING_STARTED.md @@ -0,0 +1,122 @@ +# Getting started with Telperion + +Telperion turns a *family of mathematical statements* into **Lean 4 proofs that +Mathlib's kernel re-checks from scratch**. You describe the family; Telperion +certifies each instance in exact rational arithmetic, emits Lean, and the Lean +kernel is the sole thing you have to trust. This guide takes you from a clean +machine to **an emitted certificate you have verified locally end-to-end**. + +There are two halves, and you can stop after the first: + +1. **Generate** — pure Python (sympy only). Fast, no Lean required. +2. **Verify** — compile the emitted Lean against a pinned Mathlib. This is the + step that actually makes it a proof, and it is the part newcomers most often + skip because the toolchain setup is not obvious. It is written out in full below. + +## 1. Install the Python package + +Telperion requires **Python ≥ 3.11**. From the repository root: + +```bash +pip install -e telperion # the engine (sympy-only core) +``` + +Optional extras, installed as needed: + +```bash +pip install -e "telperion[dev]" # pytest + numpy + networkx (run the test suite) +pip install -e "telperion[sdp]" # cvxpy — the SDP certificate finders +pip install -e "telperion[bg]" # numpy + networkx — the Brualdi–Goldwasser research lab +pip install -e "telperion[mcp]" # expose Telperion to LLM agents over MCP +``` + +This installs two console commands: `telperion` (the CLI) and `telperion-mcp` +(the MCP server). Check it works: + +```bash +telperion --help +``` + +## 2. Generate a certificate (no Lean needed) + +Every example is a self-contained `generate.py`. The simplest non-research one +proves Bernoulli's inequality `(1 + x)^k − 1 − kx ≥ 0`: + +```bash +cd telperion +python examples/bernoulli/generate.py +# → wrote Bernoulli (5 theorems); input hash 3aa1dbc9… +``` + +That wrote `examples/bernoulli/lean/BernoulliSolution.lean` — real Lean, one +theorem per instance, each with a proof term. You can read it; you do **not** +have to trust the generator that wrote it, because the next step makes the Lean +kernel re-prove every line. + +Re-running `generate.py --check` instead of writing verifies the output is +**byte-identical** to what's committed (this is the drift gate CI runs): + +```bash +python examples/bernoulli/generate.py --check +# → check: OK (regeneration matches frozen output byte-for-byte) +``` + +## 3. Verify the emitted Lean locally (the step that matters) + +Compiling the emitted Lean needs **Lean 4 `v4.32.0`** (the pin every example +shares) and a **pre-built Mathlib cache** — do *not* let it compile Mathlib from +source, which takes hours. + +**3a. Install elan** (the Lean toolchain manager). `lake` will read each +example's `lean-toolchain` file and fetch the exact pinned Lean automatically: + +```bash +curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh +# restart your shell, or: source ~/.elan/env +``` + +**3b. Fetch the prebuilt Mathlib oleans, then build:** + +```bash +cd telperion/examples/bernoulli/lean +lake exe cache get # downloads the prebuilt Mathlib cache (minutes, not hours) +lake build # the Lean kernel re-checks every emitted theorem +``` + +A clean exit from `lake build` means the kernel accepted every proof. That is +the whole guarantee: **a wrong certificate is a compile error, never a false +theorem.** Try it — edit a numeric constant in `BernoulliSolution.lean` and +re-run `lake build`; the kernel rejects it. + +Every example under `telperion/examples/*/lean/` follows this identical +`lake exe cache get && lake build` pattern. + +### Optional: independent second check (the Comparator) + +For an even stronger check — that the emitted proof proves *exactly* the stated +theorem using only whitelisted axioms — Telperion integrates +`leanprover/comparator` (from `openai/ten-proofs`) and the independent `nanoda` +Rust kernel. See [`COMPARATOR.md`](COMPARATOR.md). This is what the +`telperion-comparator` CI job runs; it is not required for local use. + +## 4. Use it on your own problem + +The end-to-end API is `certify → validate → emit`, then `lake build` in your own +Lean project. The five-minute in-memory example and the full list of certificate +shapes are in the [Telperion README](../README.md); the internals and the +engine/research-lab boundary are in [`ARCHITECTURE.md`](ARCHITECTURE.md); how to +add a new certificate shape is in [`../CONTRIBUTING.md`](../CONTRIBUTING.md). + +## Troubleshooting + +- **`lake build` starts compiling Mathlib from source** — you skipped + `lake exe cache get`, or your Lean version doesn't match the cache. Confirm + `lean-toolchain` reads `leanprover/lean4:v4.32.0` and re-run the cache fetch. +- **`telperion` command not found** — the `pip install -e telperion` didn't put + the console script on your `PATH`; use `python -m telperion.cli` instead. +- **`ModuleNotFoundError: cvxpy` / `networkx`** — install the matching extra + (`[sdp]` for cvxpy, `[bg]`/`[dev]` for networkx). The sympy-only core never + needs them; only the SDP finders and the research lab do. + +`conjecture1_proved = False` — nothing here depends on trusting Telperion; the +Lean kernel is the arbiter.