Lean deep-dive: stress-test the proof-assistant park in dn-research-register — coverage, bridge, cost, and the agent-era premise

[ascalva]

The ask (owner, 2026-08-09): dn-research-register (the research-register design note, PR #47, open) parks Lean/proof-assistant adoption with default not adopted and re-entry a claim a property test cannot falsify. The owner: "I didn't really see much in there about Lean — I think it's worth a deeper investigation." This issue is that investigation, pulled forward by owner directive rather than waiting on the park's re-entry condition.

What to establish or falsify:

1. Coverage — does Mathlib 4, today, actually carry the palace's objects: graph Laplacian + positive semidefiniteness, the spectral theorem, algebraic connectivity, Boolean algebras (the memberships store is a finite multiset relation over one), semirings, inner-product spaces, optimal transport / W₁ (Ollivier-Ricci's substrate, core/kernel/complex/curvature.py), Cheeger-type inequalities (core/graph/conductance.py, core/complex/cut.py)?
2. The bridge — the honest Python↔Lean gap: what exists between "prove the math, property-test the code" (the note's current posture) and verified kernels? Statement-only formalization, Plausible property testing inside Lean, float/IEEE-754 formal semantics, extraction reality.
3. The agent-era premise — the park's unstated premise is that formalization is expensive in human time. The palace's builders are LLM agents; the state of LLM-driven Lean proof/autoformalization in mid-2026 may invalidate the premise. Establish the current state with verified sources.
4. Ops cost — toolchain (elan/lake, Mathlib cache) in CI as a verdict job; maintenance burden across Mathlib versions.
5. The learning axis — the owner's stated motive for the register includes learning research language; Lean-as-curriculum (Natural Number Game → Mathematics in Lean → formalizing the palace's own laws ledger) may serve it directly.

Deliverable: a claim-ladder-disciplined report (per the register's own §2.3, eating the dogfood) as a comment on this issue, external claims verified per the external-grounding gate — plus, if findings warrant, a proposed revision to the parked row on PR #47's open branch (an adoption ladder with per-rung falsifiers replacing the flat park), presented for the owner's call, never self-applied to the note without his direction.

Grounding at HEAD (68d8d39 + staged): no .lean anywhere in the repo. First-candidate surfaces, in blast-radius order: core/stores/memberships.py (staged — Boolean-algebra/multiset laws, already spec-headed OBJECT/INVARIANT), core/kernel/complex/laplacian.py (laplacian_sym), core/complex/spectral.py (Fiedler λ₂, eigengap, normalized cut), core/graph/conductance.py (L⁺ effective resistance, heat kernel), core/kernel/complex/curvature.py (Ollivier-Ricci over W₁).

Related: #47 (the note carrying the park) · #46 (the ACM re-verification sibling — same external-grounding discipline).

[ascalva]

Lean deep-dive — investigation report (2026-08-09)

Written in the claim ladder of dn-research-register §2.3 (eating the dogfood): every
finding carries its label and its verification status. External claims verified today
unless marked otherwise; sources at the end.

The question: can Lean earn a place in the palace — at which rung, at what cost —
and does the agent era invalidate the premise behind the flat park in
dn-research-register (PR #47: default not adopted, re-entry a claim a property test
cannot falsify)?

The answer in one line: the park's premise — formalization is expensive in human
time — is stale; the honest replacement is a four-rung adoption ladder whose first rung
(Lean statements as machine-checked specs, counterexample-tested by Plausible) is one
build session, and whose costs are now denominated in the palace's own currency: agent
sessions plus owner review.

---

Axis A — Mathlib coverage of the palace's actual objects

Targets grounded at HEAD (68d8d39 + staged): core/stores/memberships.py (Boolean/
multiset relation laws), core/kernel/complex/laplacian.py (laplacian_sym),
core/complex/spectral.py (Fiedler λ₂, per-component clustering),
core/graph/conductance.py (L⁺ effective resistance, heat kernel),
core/kernel/complex/curvature.py (Ollivier-Ricci over W₁). No .lean exists anywhere
in the repo.

object	Mathlib status	evidence
graph Laplacian, PSD	present	SimpleGraph.lapMatrix, isPosSemidef_lapMatrix — Observation, VERIFIED 2026-08-09
components = Laplacian nullity	present	card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix — VERIFIED; this is exactly the theorem spectral.py's per-component contract rests on
spectral theorem (Hermitian)	present	Matrix.IsHermitian.spectral_theorem, real eigenvalues, eigenvectorBasis, rank = nonzero eigenvalues — VERIFIED
Boolean algebras, lattices, Finset/Multiset	bedrock	the BooleanAlgebra hierarchy — the memberships laws' entire substrate. Stone duality proper sits at the frontier (an LFTCM2024 workshop project built Profiniteᵒᵖ ≌ BoolAlg); not needed for laws
semirings, inner-product spaces	bedrock	core algebra/analysis hierarchy [FROM MEMORY — uncontroversial; spot-verify at build time]
W₁ / Kantorovich–Rubinstein	absent from Mathlib, formalized against it	arXiv:2607.08986 ships W₁ properties + KR duality as a self-contained 49-declaration layer behind a 22-declaration interface, compiling against Mathlib alone — borrowable prior art, VERIFIED
Cheeger-type inequalities	absent	no Mathlib module found (searches return only the informal literature). The palace's conductance.py uses Φ(S) and R_eff definitions, not the inequality itself — the definitions formalize cheaply; the inequality is future work only if a claim ever depends on it
Ollivier-Ricci curvature	absent	would need finite-support W₁ (a finite LP); the KR layer above is the on-ramp. A project, not free — and not rung-1 work

Claim A (supported): every law the memberships store and the Laplacian layer would
put in a laws ledger has its proof substrate already in Mathlib; the spectral layer's
load-bearing theorems are present by name. The genuinely missing pieces (Cheeger,
Ollivier-Ricci) sit exactly where the palace's code invokes definitions, not theorems.

Axis B — the bridge (Lean never proves the NumPy)

The translation gap is real and stays real: Lean proves the mathematics; the Python is
checked by tests. What narrows it, verified:

• Plausible (leanprover-community/plausible) — property-based testing inside
  Lean, tactic-integrated, QuickCheck-style (Shrinkable/SampleableExt): given a
  stated theorem it hunts random counterexamples. The falsifiers-before-proofs
  epistemology as a Lean tactic: the same statement is attacked first, proven second,
  in one artifact. — VERIFIED
• Float formalization exists now: FloatSpec (a Flocq-mirroring IEEE-754
  formalization in Lean 4 + Mathlib, executable reference functions), ryu-lean4
  (complete binary64 roundtrip proof), TorchLean's IEEE32Exec (bit-level binary32
  incl. subnormals/NaN/rounding). The register's float-ε rule has formal substrate —
  though ε-bound claims about our pipelines remain expensive (rung L3, below). — VERIFIED
• The working bridge remains two-sided falsification [Inference]: Lean states and
  proves the law over exact arithmetic; Hypothesis property-tests the NumPy against the
  same law with tolerance bounds; the two artifacts cross-reference by law id. One law,
  two independent attack surfaces.

Axis C — the agent-era premise (the crux)

Observation, VERIFIED: arXiv:2607.08986 (July 2026) formalized the full mean-field
derivation of the Vlasov equation in Lean 4 + Mathlib with a mathematician directing
an AI system — "the human's role was to direct, not to write proofs." Headline theorems
in ~a week; the complete 299-declaration development in ~a month.

Observation, VERIFIED: the mid-2026 prover ecosystem is repository-scale:
Goedel-Prover-V2 at 92.2% on miniF2F (52.94% pass@1), DeepSeek-Prover-V2, Kimina-Prover,
Aristotle; multi-agent Lean pipelines (decompose → probe for counterexamples → prove
sub-lemmas → assemble under kernel control) that mirror the palace's own orchestration
shape.

The honest limitation, stated: the "definition-finding gap" — no system yet
autonomously proposes and proves novel research mathematics. Irrelevant to rungs L1–L2
below: formalizing known structure laws (Boolean algebra, PSD, spectral) is exactly
the regime today's provers are strong in.

Claim C (supported): the park's premise is invalidated. Formalization cost is now
agent-session-denominated — the same currency as every other palace deliverable — with
the owner reviewing Lean the way he reviews Python: on the PR, with the kernel as a
fifth CI verdict that cannot be sweet-talked.

Axis D — ops cost

• CI: official leanprover/lean-action — elan install, lake build/test/lint,
  Mathlib cache (lake exe cache get), GitHub caching, macOS runners. A formal/ lake
  package downstream of Mathlib gets tractable CI minutes via the cache. — VERIFIED
• Boundary [Inference, load-bearing]: formal/ is a sibling package like eval/
  — never imported by core/, importing nothing from it. Core self-containment is
  untouched; the spec layer is documentation-with-a-kernel-check, zero runtime coupling.
• Maintenance, priced honestly: Mathlib moves fast; the toolchain is pinned
  (lean-toolchain) and bumped deliberately as a chore. A statements-only L1 layer has
  small API surface (order/lattice/matrix basics) and low churn exposure.

Axis E — the learning axis (the owner's stated motive)

The curriculum writes itself and every rung produces palace artifacts rather than
exercises: Natural Number Game → Mathematics in Lean (both community-standard) → state
the memberships laws (L1) → discharge them (L2). The register's lexicon gains entries
whose "research meaning" column is machine-checked rather than recalled. [Inference:
this serves the "a little for me" motive in owner seed 2 more directly than any
glossary can — you learn a register fastest by having a kernel reject your misuse of it.]

---

The proposal — replace the flat park with a ladder

• L0 — today. Nothing. (The flat park's default.)
• L1 — statements as specs. One build-plan-sized unit: formal/ lake package;
  Lean statements of the laws ledger's first laws (memberships' Boolean/multiset laws;
  laplacian_sym PSD + zero row sums; L⁺ symmetry/PSD), each carrying a Plausible
  counterexample attack; proofs taken where Mathlib gives them in one line, sorry
  elsewhere — but sorry-count is a ratchet, monotone down. CI via lean-action as an
  advisory job first. Falsifier for the rung itself: if the statement layer never
  catches a mis-stated law that Hypothesis alone missed, by the third law batch, L1 is
  decoration and retracts to L0.
• L2 — proofs of the finite/algebraic core. Discharge L1 obligations over exact
  arithmetic; agent-authored under supervision (the Vlasov workflow at palace scale).
  Unlocks the ladder's Theorem rung honestly: Theorem (machine-checked, formal/...)
  — the rung dn-research-register expects to stay empty becomes reachable without
  lowering its price.
• L3 — numerical bridge. Float-ε claims via FloatSpec-style models. Expensive;
  entered per-claim, only where a design claim demands a machine-checked ε-bound.
• L4 — verified kernels. Stays parked. Research-grade; no palace claim needs it.

Where it lands [the design boundary, per dn-research-register §1.3]: the ladder is
foundations-arc substance — it belongs in the sibling mathematical-foundations design
note (the laws ledger's formal layer), not in the register note. The register note's
parked row should then point at the ladder instead of carrying a flat "not adopted":
default L0, ladder specified in the foundations note; re-entry for L1 the laws
ledger's first laws exist to state.

Sources

• Mathlib docs: LapMatrix · Matrix.Spectrum · Hermitian
• arXiv:2607.08986 — Vlasov formalization, AI-assisted; the W₁/KR layer and the direct-not-write workflow
• Provers: Goedel-Prover · Lean 4 survey · ICML 2026 sub-agent orchestration report · emergentmind overview
• Tooling: leanprover-community/plausible · leanprover/lean-action · Mathlib-as-dependency
• Float: FloatSpec · ryu-lean4 · TorchLean
• Stone duality frontier: LFTCM2024 BooleanDuality
• Cheeger-in-Mathlib absence: no module surfaced across targeted searches (informal-literature hits only) — recorded as absent, re-checkable cheaply.