Certificate-emitting solvers for equational implication over magmas. Christopher Brock · Riemann Labs · SAIR Foundation Mathematics Distillation Challenge, Stage 2
No answer counts unless the judge accepts it. Every claim in this repository is a machine-checkable Lean 4 certificate re-verified by the competition's open, deterministic judge — or it isn't a claim.
| Entry | File | Philosophy |
|---|---|---|
| EULER | SHIP-2026-08-26/solvers/EULER.py |
Precomputed mathematics: an exact direction oracle from public ETP data, a hypothesis-keyed finite-model bank, bounded Knuth–Bendix completion, transitivity composition, and ATP-proof replay. |
| WILL | SHIP-2026-08-26/solvers/WILL.py |
The deliberate counterpart — no oracle, no banks, no borrowed certificates. Technique only. |
The gap between them is the finding. EULER measures what accumulated public mathematics (sediment) buys; WILL measures what live reasoning (technique) achieves alone. The study of that gap is the competition paper, Sediment and Technique.
Both are single-file, Python 3.11 stdlib-only, under 500 KB, valid for the Solo and Marathon tracks, with embedded-data disclosures inline.
- The submission packet — frozen 2026-08-26:
solvers, papers, evidence,
CHECKSUMS.sha256. - How we built it · How to check it
- Submission notes — per-entry disclosures, honest scope, acknowledgments.
- Mathematics in the Age of Mechanical Reproduction — the epistemic framework: what it means to know a theorem when machines produce the proofs.
- EULER: a certificate-emitting solver — the architecture paper.
- Sediment and Technique — the EULER-vs-WILL controlled study.
Supporting: EULER methodology · trust framework · WILL manifesto · the full contribution pack (manifest, four tellings, statement fidelity, epistemic badges, trace, workflow diagrams).
Standalone Lean 4 files that compile against the competition judge, ordered from the simplest technique to the most compositional:
| # | File | Pair | Technique |
|---|---|---|---|
| 1 | RiemannLabs_Proof_1_Constancy.lean |
3268 → 3253 | Direct constancy substitution |
| 2 | RiemannLabs_Proof_2_ConstantCollapse.lean |
3829 → 41 | Constant magma via transitivity |
| 3 | RiemannLabs_Proof_3_Bootstrap.lean |
359 → 4065 | Self-referential bootstrap (congr_arg) |
| 4 | RiemannLabs_Proof_4_Pivot.lean |
404 → 4236 | Shared pivot (.trans / .symm) |
| 5 | RiemannLabs_Proof_5_CompoundSubstitution.lean |
282 → 2133 | Compound term substitution |
- Held-out cohorts — problems the solvers had never seen, with provenance and a reproduction script.
- Aristotle provenance — job records for every proof queued to the Aristotle/Harmonic prover.
- WILL bench — self-tests, manifests, and the Lean certificates behind WILL's numbers.
- Solver test environment — the AXLE judge replica (cloud Lean 4.32.2, the judge's exact toolchain), TRUE/FALSE benches, and vendored problem sets. The ground-truth outcome table is deliberately absent — see the anti-cheating note.
- Judge bug report — the olean-header mismatch we found and reported during Stage 2.
- Domain: 4,694 equational laws over magmas; ~22 million pairwise implications. Built on the equational_theories project (Tao et al.) and the SAIR Stage 2 judge.
- Verification: Lean 4 kernel — machine-checked, zero trust.
- Riemann Labs is the mathematical research division of the Brock Command Center — formal verification, automated reasoning, and the intersection of algebraic structure with computational proof. See the Riemann Labs observatory and our machine-verified mathematics corpus (11,000+ AXLE-kernel-verified Lean 4 theorems).
- Brockian ↔ equational-theory connections · AI-orchestrated mathematics whitepaper
Frozen ship: SHIP-2026-08-26.zip ·
SHIP-2026-08-26.FREEZE.sha256