Demonstrandum is a verification-first, multi-agent AI mathematics pipeline, directed and audited by John Erlbacher (Independent Researcher). Its house rule is that no claim is ever accepted on an AI's word: the unit of progress is an artifact on disk plus an independently written checker that accepts it. Every result below is mechanically checkable by a reader with zero trust in any AI or in the author.
Wave 1 delivered 13 verified results — 11 refutations of published conjectures, one proof of a published conjecture, and one numerical record — each frozen verbatim from its source before attack and backed by a runnable certificate or a Lean 4 proof accepted by the kernel.
Results
| Result | Grade | Artifact |
|---|---|---|
| IRIS Conjecture 6.1 ("NuevaMirada") — refuted | dual-checker | RESULTS.md |
| Discrete Borsuk Conjecture 3 (arXiv:2508.20009) — disproved in Lean 4 | kernel | paper |
| Graffiti Conjecture 143 — refuted | dual-checker | paper |
| Graffiti Conjecture 154 (std-dev reading) — refuted | dual-checker | paper |
| TxGraffiti / Davila Conjecture 9 — refuted | dual-checker | RESULTS.md |
| Pandey parity conjecture — refuted (both directions) | dual-checker | RESULTS.md |
| Solubilizer Conjecture A.1 (arXiv:2412.16177) — refuted | dual-checker | RESULTS.md |
| Solubilizer Conjecture A.13 — refuted | audit-panel | RESULTS.md |
| Solubilizer Conjecture A.16 — refuted | audit-panel | RESULTS.md |
| Sun Conjecture 4.6 (arXiv:2108.07723) — refuted at p = 29 | dual-checker | paper |
| Koch–Narayan Conjecture 1 — refuted | dual-checker | RESULTS.md |
| C(13) ≥ 36 record ("no 5 on a sphere") — improves C(12) ≥ 33 | dual-checker | paper |
| Elizalde–Luo {1132, 3312} conjecture — proved in Lean 4 | kernel | paper |
kernel — the entire claim is a Lean 4 theorem accepted by the Lean kernel under only the three standard mathlib axioms. dual-checker — certificate accepted by ≥ 2 independently written checkers plus mutation testing. audit-panel — banked runnable checker plus adversarial clean-room audits across model families. Exact statements, verbatim frozen sources, and a per-result "what this does not show" caveat are in RESULTS.md.
Verify it yourself
The complete wave-1 bundle carries a one-command master verification battery. No trust required.
git clone https://github.com/demonstrandum-research/artifacts.git
cd artifacts
python verify_all.py # default battery: 33 checks, ~5-15 min
python verify_all.py --strict # SKIPs become failures (full zero-trust mode)
python verify_all.py --list # list all checks; --only SUBSTR runs a subsetRequirements: Python 3.10+ with numpy and sympy. A SKIP always means "not verified on this machine" — the summary says so loudly. See VALIDATION.md for what each check does and does not establish.
Papers
Eight papers accompany the results. Each carries LaTeX source, compiled PDF, build notes, referee-round responses, and recompute scripts. The archived, citable snapshot is on Zenodo.
Archived snapshot (DOI)
10.5281/zenodo.21264100 — Demonstrandum verified artifacts: eight papers in combinatorics (v2). Discrete Borsuk, Elizalde–Luo, Sun 4.6, no-5-on-a-sphere record, Graffiti 143 & 154, and the union-closed-sets flagship, plus verification code bundles.
Source & verification battery
github.com/demonstrandum-research/artifacts — complete artifact repository: certificates, independent checkers, mutation suites, Lean projects, and verify_all.py.
Methods & AI-use disclosure
Results are produced by a multi-agent workflow built on Claude language models (Anthropic), with adversarial cross-checks by a different model family (OpenAI Codex/GPT). AI agents propose constructions, write checkers and proofs, and audit each other under a protocol in which nothing is accepted on a model's word: every accepted claim is backed by a machine-verifiable artifact (certificate plus independent checkers, or a Lean proof accepted by the kernel). Statements are frozen verbatim from their authoritative sources before any attack. A human — the author — directs the campaigns, audits every gate, and takes full responsibility for the claims.