>_PAPER.PROOF.CODE

Betti DiscoveryMulti-Agent Algebraic-Topological Invariant Discovery

Formal Lean 4 proofs certifying the provability oracle used by a multi-agent system that autonomously discovers Betti numbers and Euler characteristic from triangulated surface data. Based on the open challenge of recovering homology from polyhedral data using only knowledge of linear algebra.

arXiv:2603.04528 GitHub|IPFS: bafybeiexph6w6zx...

Original Researchers

Daattavya Aggarwal

PhD Student, equal main author

Department of Computer Science and Technology, University of Cambridge

Oisin Kim

PhD Student, equal main author

Department of Computer Science and Technology, University of Cambridge

Carl Henrik Ek

Professor of Statistical Learning

Department of Computer Science and Technology, University of Cambridge

Challenger Mishra

Departmental Early Career Academic Fellow

Department of Computer Science and Technology, University of Cambridge

All authors: University of Cambridge. Paper: arXiv:2603.04528v1 [cs.AI] 4 Mar 2026.

Lean 4 Modules

RankNullityPremises + SRTranslation

Certified Theorems

sphereEuler, torusEuler, twoComponentB0

Predicate Templates

rankNullity, connected, orientable, betti, etc.

Sorry Count

All proofs complete (omega / simpa)

186

Lines of Lean

124 + 62 across 2 modules

C Files

rank_nullity_premises.c + sr_translation.c

Rust Tests

All passing (0 failures)

Surface Types

Sphere, torus, Klein bottle, disjoint union

>_VERIFICATION.SEAL

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

3 THEOREMS VERIFIED2 MODULES186 LINES0 SORRY

Betti Discovery • Lean 4 + Mathlib • Apoth3osis Labs

Key Mathematics

GF(2) CHAIN COMPLEX

C_2 \xrightarrow{\partial_2} C_1 \xrightarrow{\partial_1} C_0

Boundary matrices d1 (V×E) and d2 (E×F) over the two-element field. 8 features extracted via Gaussian elimination.

EULER CHARACTERISTIC

\chi = V - E + F = \sum_{i=0}^{2} (-1)^i \, b_i

BETTI NUMBERS

b_0 = \dim(V_0) - \operatorname{rank}(\partial_1), \quad b_1 = \operatorname{null}(\partial_1) - \operatorname{rank}(\partial_2), \quad b_2 = \operatorname{null}(\partial_2)

PROVABILITY ORACLE

\rho(s) := \begin{cases} 1 & \text{if } A \text{ finds a proof for } s \text{ before timeout} \\ 0 & \text{otherwise} \end{cases}

Deterministic template matching against 5 formally verified Lean 4 theorems. No neural network, no heuristic.

Paper ↔ Proof Correspondence

PAPER	PROOF	STATUS	NOTES
§1.2 Euler's conjecture for polyhedra	sphereEuler, torusEuler	PROVED	Chi = V - E + F for sphere (=2) and torus (=0)
§1.7 Learning problem and mathematical background	rankNullityD1, rankNullityD2	PROVED	Rank-nullity over arbitrary division rings and finite-dimensional modules
§1.10 Conjecturing agent	SRTranslation (AST, render, featureArity)	PROVED	Symbolic regression expression tree with 8 features and 5 operators
§1.11 Skeptical agent	N/A (implemented in Python)	N/A	Attention steering over data distribution — runtime component
§1.12 Environment and provability	vanishingMiddleBetti, bettiOneValue2, twoComponentB0	PROVED	Certified provability oracle: 5 theorem templates
§2.1 Premises and data (D₀–D₃)	N/A (Python surface generators)	N/A	Sphere, torus, Klein bottle, disjoint union generators
§2.2–2.4 Ablation results	evaluate.py (4-variant ablation)	N/A	M₀ (full), M₁ (no oracle), M₂ (no SA), Only CA

>_PROOF.BLUEPRINT

Proof Blueprint

⊢⊣⊢⊣

>_MENTAT.JOIN

“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune

A janitor who proves a theorem outranks a tenured professor who publishes noise.

Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

Ethics, review & quality assurance

Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. RankNullityPremises depends on Mathlib for linear algebra primitives; SRTranslation uses only the standard library.

Foundation Core Moduleimports

>_VERIFIED.C

Verified C Artifacts

Generated via CAB pipeline: Lean 4 → LambdaIR → MiniC → C. Each file carries a correctness certificate verifying semantic preservation.

rank_nullity_premises.c

5 certified theorem templates + 3 theorem functions | from RankNullityPremises

DOWNLOAD

sr_translation.c

SR expression tree: tagged union + render + featureArity | from SRTranslation

DOWNLOAD

>_SAFE.RUST

Safe Rust Artifacts

Transpiled from verified C to idiomatic safe Rust. Raw pointers replaced with owned types, slices, and iterators. Correctness inherited from the C verification chain. Download the full crate (includes Cargo.toml and lib.rs) and run cargo test.

rank_nullity_premises.rs

ChainDimensions struct + Betti computation + 7 tests | from RankNullityPremises

DOWNLOAD

sr_translation.rs

SRExpr enum + Display + featureArity + 4 tests | from SRTranslation

DOWNLOAD

lib.rs

Crate root re-exporting both modules | from —

DOWNLOAD

Cargo.toml

Package manifest (edition 2021, 0 dependencies) | from —

DOWNLOAD

>_PROVENANCE

Provenance Chain

Research Paper

Aggarwal, Kim, Ek & Mishra. “Discovering mathematical concepts through a multi-agent system.” arXiv:2603.04528, March 2026. Multi-agent framework for computational mathematical discovery from polyhedral data.

Lean 4 Formalization

2 modules, 3 theorems, 186 lines. Certified provability oracle for Betti numbers and Euler characteristic + SR expression AST. Mathlib dependency. Zero sorry/admit.

CAB-Certified C

Lean 4 → LambdaIR → MiniC → C. Each transformation step carries a certificate hash verifying semantic preservation. gcc -std=c11 -Wall -Wextra -Werror: 0 warnings.

Safe Rust

C → Rust transpilation. Ownership semantics, no unsafe blocks. Correctness inherited from verified C source. cargo test: 11/11 pass.

IPFS Pinned

All artifacts content-addressed and pinned to IPFS. CID: bafybeiexph6w6zx4r3wq7muuqxrbrx64ouho33v3bwxkngcjdhu3yjnida. Immutable, globally retrievable via any IPFS gateway.

>_IPFS.STORAGE

IPFS Permanent Storage

All artifacts content-addressed and pinned to IPFS. Immutable, globally retrievable via any IPFS gateway. No server dependency — the proofs persist on the distributed web.

Paper (PDF)Lean Proofs Verified C Safe Rust ALL (IPFS)

Root CID: bafybeiexph6w6zx4r3wq7muuqxrbrx64ouho33v3bwxkngcjdhu3yjnida

>_DOWNLOAD

Download Archives

📄Paper (PDF)📜Lean Proofs 💻Verified C ⚙️Safe Rust

All proofs machine-verified using Lean 4 and Mathlib

Betti DiscoveryMulti-Agent Algebraic-Topological Invariant Discovery

Original Researchers

Formal Verification Certificate

Key Mathematics

GF(2) CHAIN COMPLEX

EULER CHARACTERISTIC

BETTI NUMBERS

PROVABILITY ORACLE

Paper ↔ Proof Correspondence

Proof Blueprint

A janitor who proves a theorem outranks a tenured professor who publishes noise.

Module Dependencies

Verified C Artifacts

Safe Rust Artifacts

Provenance Chain

IPFS Permanent Storage

Download Archives

All Projects

Betti Discovery (GitHub)

Lean Blueprint