Apoth3osis
>_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.04528GitHub|IPFS: bafybeiexph6w6zx...

Original Researchers

Daattavya Aggarwal
Daattavya Aggarwal
PhD Student, equal main author
Department of Computer Science and Technology, University of Cambridge
Oisin Kim
Oisin Kim
PhD Student, equal main author
Department of Computer Science and Technology, University of Cambridge
Carl Henrik Ek
Carl Henrik Ek
Professor of Statistical Learning
Department of Computer Science and Technology, University of Cambridge
Challenger Mishra
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.

2
Lean 4 Modules
RankNullityPremises + SRTranslation
3
Certified Theorems
sphereEuler, torusEuler, twoComponentB0
8
Predicate Templates
rankNullity, connected, orientable, betti, etc.
0
Sorry Count
All proofs complete (omega / simpa)
186
Lines of Lean
124 + 62 across 2 modules
2
C Files
rank_nullity_premises.c + sr_translation.c
11
Rust Tests
All passing (0 failures)
4
Surface Types
Sphere, torus, Klein bottle, disjoint union
>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED3 theorems • 0 sorry2 modules0 SORRY

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

C2→∂2C1→∂1C0C_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

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

BETTI NUMBERS

b0=dim⁡(V0)−rank⁡(∂1),b1=null⁡(∂1)−rank⁡(∂2),b2=null⁡(∂2)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

ρ(s):={1if A finds a proof for s before timeout0otherwise\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

PAPERPROOFSTATUSNOTES
§1.2 Euler's conjecture for polyhedrasphereEuler, torusEulerPROVEDChi = V - E + F for sphere (=2) and torus (=0)
§1.7 Learning problem and mathematical backgroundrankNullityD1, rankNullityD2PROVEDRank-nullity over arbitrary division rings and finite-dimensional modules
§1.10 Conjecturing agentSRTranslation (AST, render, featureArity)PROVEDSymbolic regression expression tree with 8 features and 5 operators
§1.11 Skeptical agentN/A (implemented in Python)N/AAttention steering over data distribution — runtime component
§1.12 Environment and provabilityvanishingMiddleBetti, bettiOneValue2, twoComponentB0PROVEDCertified provability oracle: 5 theorem templates
§2.1 Premises and data (D₀–D₃)N/A (Python surface generators)N/ASphere, torus, Klein bottle, disjoint union generators
§2.2–2.4 Ablation resultsevaluate.py (4-variant ablation)N/AM₀ (full), M₁ (no oracle), M₂ (no SA), Only CA
>_PROOF.BLUEPRINT

Proof Blueprint

>_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.

FOUNDATIONCORE MODULEMathlibStdRankNullityPremisesSRTranslation
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.

C

rank_nullity_premises.c

5 certified theorem templates + 3 theorem functions | from RankNullityPremises

DOWNLOAD
C

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.

Rs

rank_nullity_premises.rs

ChainDimensions struct + Betti computation + 7 tests | from RankNullityPremises

DOWNLOAD
Rs

sr_translation.rs

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

DOWNLOAD
Rs

lib.rs

Crate root re-exporting both modules | from —

DOWNLOAD
Rs

Cargo.toml

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

DOWNLOAD
>_PROVENANCE

Provenance Chain

1

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.

2

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.

3

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.

4

Safe Rust

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

5

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 ProofsVerified CSafe RustALL (IPFS)

Root CID: bafybeiexph6w6zx4r3wq7muuqxrbrx64ouho33v3bwxkngcjdhu3yjnida

>_DOWNLOAD

Download Archives

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

All Projects

Back to the Paper → Proof → Code index.

Betti Discovery (GitHub)

Standalone Python implementation with multi-agent discovery game.

Lean Blueprint

Full HeytingLean proof corpus and dependency graph.

Betti Discovery | Paper → Proof → Code | Apoth3osis

All proofs machine-verified using Lean 4 and Mathlib