Input
A claim, the example that’s supposed to prove it, a link to where it came from, and a check precise enough for a computer to run.
Public verification release · v1
A model can suggest
the next step. It cannot
grade its own work.
In math, a witness is the concrete example that backs a claim—here, an actual list of 23 points. Erdős Check inspects the witness and issues a portable receipt: exactly what was checked, by which independent algorithms, and whether the record replays.
Today: verify, not discover. One public contract. One known-result calibration, which the search failed — it reached 20 points where the published bound is 23, so the engine stays in verify mode and makes no claim at larger n. No optimality claim.
WITNESS / C(8) ≥ 23
receipt available
POINTS23 unique
SUBSETS33,649 / 33,649
RESULTPASS / exact
Your browser · a fourth implementation
recomputing…
0 / 33,649 five-point subsets
Not a download and not the Python bundle — the 5×5 in-sphere determinant of every subset, recomputed from scratch here in exact-integer BigInt. Each one must be non-zero. Same Bareiss elimination as the bundle's first verifier, rewritten in BigInt and run on your machine — a different language and a different process, not a fourth method. read the code ↗
01 / CONTRACT
The label
A narrow promise,
enforced all the way down.
Give Erdős Check a concrete example—the witness—and an explicit contract for what “checked” means. It returns a portable receipt, or refuses to promote the claim.
Output
A versioned receipt with measured checks, independent verifier results, artifact hashes, limits, and a replay audit.
Refusal
Malformed evidence, a broken lineage, verifier disagreement, an incomplete check count, or an inflated claim stops promotion.
02 / PUBLIC SPECIMEN
A receipt you can interrogate
Published construction.
Fresh verification.
CLAIM / EXISTENTIAL LOWER BOUND
C(8) ≥ 23
A published set places 23 points in an 8×8×8 integer grid with no five on one sphere or plane.
Was the witness well-formed?
23 JSON-integer points; unique; all inside {1…8}³
PASS
Was every case checked?
33,649 of 33,649 five-point subsets measured
PASS
Did three implementations agree?
Bareiss + cofactor + permutation-sum; 0 disagreements
PASS
Does the record replay?
Persisted lineage audited; witness recomputed from the persisted points, not read from a cached verdict
PASS
Established The supplied construction satisfies the declared exact-integer predicate, so it supports the lower bound C(8) ≥ 23.
Not established Erdős Check did not discover this construction. This does not prove C(8) = 23, optimality, or a general theorem. Three implementations agreeing rules out an arithmetic bug in one of them; all three ask the same question — that five points are cospherical or coplanar exactly when the lifted 5×5 determinant is zero — so agreement is not a test of the predicate itself.
03 / SO WHAT
The result is known.
Proposing and grading
are different jobs.
The dangerous moment in AI-assisted mathematics is not the idea. It is the promotion of an attractive answer into a trusted result.
Erdős Check treats those as different jobs. A model or human may propose a witness. A deterministic contract grades it. The public record preserves the source, computation, verdict, and scope—so the conclusion does not depend on trusting the proposer.
“Show me exactly what the machine established, and let me rerun it without the machine.”
01Propose
Human, model, search, or literature supplies a candidate. No authority granted.
02Verify
Exact, declared algorithms execute the contract and measure every required check.
03Promote
Only passing evidence earns a receipt, bounded to what the computation established.
04 / PROVENANCE
Five persisted nodes, not a magic green check
Follow the claim
to its evidence.
Select a node to inspect the recorded actor, input, output, certainty, and parent linkage. This view is populated from the downloadable ledger—not a presentation-only mock.
NODE 01LIVE
Hypothesis
- Actor
- reasoning core
- Claim
- The published 23-point construction may satisfy the declared predicate.
- Authority
- None. A hypothesis starts the check; it does not settle it.
Two different things happen during verification.
Ledger audit: cached lineage is checked with zero tool re-executions. Mathematical recheck: the persisted witness is recomputed from the points across all 33,649 subsets, not read from a cached verdict. Both must pass.
05 / TRUST BOUNDARY
What exists.
What does not.
Implemented
- Fail-closed public receipt contract for the supported C(8) witness
- Three exact-integer determinant implementations
- SQLite lineage, JSON export, artifact hashing, and strict replay audit
- Lean result gate (code path present; not exercised by this release — see receipt.json)
Experimental
- Finite search drivers and operator-directed candidate generation
- Additional toy-problem verification contracts
- Presentation layers for broader mathematical artifacts
Not claimed
- Autonomous model reasoning or unsupervised research
- Verification of arbitrary mathematics
- Novel discovery, optimality, or formal proof for this release
06 / REPRODUCE
Take the evidence with you
One bundle.
One offline command.
The release includes the witness, pinned source notebook, SQLite run, ledger export, verifier source, hashes, and a standard-library verification entry point.
python verify_release.py receipt.json --strictThe construction is sourced from Google DeepMind’s AlphaEvolve repository of problems at pinned commit bfd224d…. Erdős Check’s contribution here is the independent verification contract and receipt, not the construction.
For skeptical engineers, mathematicians, and AI builders
Trust the receipt.
Then try to break it.
Erdős Check is early, deliberately narrow, and working in public. If you build systems where a plausible answer is not enough, I’d like to compare notes.