Research notes · Campinas, Brazil · UTC−3
Verification for machine-generated mathematics — and for the tests that grade it
Proofs you can try to break. I am Carlos Toledo. I check numerical and
mathematical claims without trusting
how they were produced — a language model’s, a published paper’s, or my own
— and the answer is either a certified enclosure that provably contains the true value,
or a plain statement that the check did not close. The same question turned on the graders
themselves: given a test suite, can it tell a correct answer from a plausible wrong one?
On HumanEval, 24 of 163 items could not. Every page below publishes the program that produced
its numbers — beside the page, or running live inside it — and every check has been
shown to fail on a deliberately broken copy of that program.
Three readers, three doors: if you referee or review mathematics,
start here · if you build or grade evaluations, start with
the graders, graded · if you
dispatch or price hydro, start with
a power system priced live.
Try to break one — right now, nothing installed
- this browser · ~10 sOpen the Erdős #290 page: a proved theorem
re-verifies itself live as you read. Press “break it:
(d+1) ↦ (d+2)” and the page must go red, naming the line of the
proof that noticed.
- python · ~30 sReproduce the number at the top of this
page from a clean clone — Python standard library, no network, no model.
The commands are below.
- node · ~1 minWatch a verdict flip: one run says
CERTIFIED, the same run with a planted mutant says REFUSED — proof the first
answer could have come out differently. Also below.
Start here — for a reviewer with ten minutes
Five results and one proposal. Each result comes in three lines: the
claim somebody else made, what I did to it, and what happened — the
proposal does not, because it has not happened yet. Nothing below is stronger than the page it
links to — where a check did not close, these lines say so. Dates follow the
hub’s convention: a plain date is printed by the page
itself; † marks first publication to the repository.
-
Number theory · Erdős #290 · live in the page · 2026-08-03
The proof you can attack: five exceptional
degrees, a theorem — and falsifier buttons wired to it
- The claim
- van Doorn’s published bound on Erdős #290 rests on one constant,
assembled from Galois groups — and at three degrees, d = 8, 24, 48, the
paper records the group as unidentified, bounding the missing terms by
δ ≤ 1. The author later called the needed group data an open
request.
- What I did
- Pinned all three exactly, found two more the paper never reached
(d = 80 and 120), wrote the pattern down as a conjecture, tested it blind at
k = 6 — then proved it: for even degree the exceptions are
exactly d = 4k(k+1). Recomputed the constant with every finite piece an
exact rational.
- What happened
- A certified bracket seven times narrower than the paper’s published
0.82 < c < 0.85 — and the theorem re-proves itself
live in the page, with falsifier buttons that mutate the mathematics and must turn it
red. Scope, stated: this claims no solution to #290 itself — the
asymptotics remain open.
No install: press “break it” on the page. Or run theorem.js — about
fifteen seconds, plain Node.
-
Measuring the evaluator · HumanEval · 2026-08-08
24 of 163 HumanEval items accept
a solution proved wrong — and a perfect mutation score did not predict it
- The claim
- HumanEval is a standard benchmark for code generation. A model that passes an item is
recorded as having solved it — which assumes the item’s own test suite can
tell a correct solution from a wrong one.
- What I did
- Asked that of the benchmark instead of the model, per item, with no model in the loop.
First by mutating each reference solution mechanically; then with realistic wrong
solutions, each shipping a witness — one concrete input where it provably
differs from the reference. A candidate whose witness fails to separate it is discarded
and counted in neither denominator.
- What happened
- 24 of 163 items — 14.7% — accepted a solution proved wrong. 18 of
those had been rated fine by mutation testing, and 10 of them killed every
mutant: a perfect score. Scope, stated: one benchmark, one adversary, one
candidate per item — so 14.7% is a rate for this adversary, not a constant.
Reproduce Path A in about 30 seconds, Python standard library only.
-
Computer-assisted proof · Maxwell 1873 · 2026-08-04
The AI-found counterexample to
Maxwell’s 1873 conjecture, certified: 24 equilibria where the conjecture allows
at most 16
- The claim
- Maxwell said in 1873 that five point charges admit at most 16 equilibrium points. A
2026 paper refutes him with a configuration having 24 — the idea credited to an
OpenAI model. Its evidence was floating‑point computer algebra, published with
no code artifact and no concrete ε.
- What I did
- Pinned the paper’s own Figure 1 configuration at ε = 1/6
and enclosed every critical point in outward‑rounded interval arithmetic, so each
one is proved to exist rather than found by search.
- What happened
- 24 pairwise‑disjoint boxes, each certifying existence, local uniqueness and
nondegeneracy of one critical point — and 24 > 16 in exact integers.
Scope, stated: one pinned instance. The paper’s asymptotic statement is
not audited.
Run the verifier and its mutation controls yourself.
-
Independent verification · six results · 2026-08-03
Six AI-claimed math results,
independently re-verified
- The claim
- Six mathematical results produced or assisted by AI systems. On every one, the only
check on record was the original author’s own.
- What I did
- Re-derived each from scratch in separate arithmetic sharing no code with the original,
then planted a bug in every verifier to prove it was capable of going red.
- What happened
- Five CONFIRMED on the layer checked. One PARTIAL — its machine-checkable
fragment holds, its analytic core is prose and was not audited, and the page says
so rather than letting the confirmation stand in for it. The lane re-runs in under five
seconds.
-
New certificate class · gradient structure · live in the page · 2026-08-12†
No metric, no potential
— a machine-checked certificate that a flow is not a gradient
- The claim
- A folklore fact: a gradient flow’s Jacobian at an equilibrium has real spectrum,
under any Riemannian metric. For softmax attention, the published non-gradient
statement covers one metric — Wasserstein-2, in the mean-field limit, under tied
weights.
- What I did
- Made the contrapositive machine-checkable — an exact-rational Sturm count that
certifies a complex eigenvalue pair, ruling out every metric and every potential at
once — and ran it over two preregistered enumerations: engineered
softmax-attention equilibria, and the Brusselator beside an independent exact twin.
- What happened
- 224 of 864 attention instances and 37 of 60 Brusselator instances certified; the
d = 2 slice is all-real by a theorem the census forced; the twin agreed on
all 60, and both falsifiers carry a mutation-verified red. Scope, stated: local,
Riemannian-gradient only, the criterion’s necessary half — and the claim
status on the page’s face is conjectured.
The certificate re-runs live in the page, on the same spliced kernels the batteries
gate.
-
Proposal · evaluation for automated researchers · 2026-07-31†
An eval for automated researchers that
answers in dispositions, not scores: CERTIFIED, REFUSED, HACK‑SUSPECT, or
OUT‑OF‑SCOPE
A proposal with a runnable pack, not a verified result — listed last for
that reason. A second lane beside the reward metric, for the cases where a scalar can be
gamed. Runs in about a minute with Node and nothing else: one command scores a held-out
fixture, a second plants a mutant to prove the lane can say no.
How a result earns a green light
The house method — not a report, the rule every report obeys
The house rule is that green proves nothing until it can go red. Three obligations,
on every page here:
-
Every certificate ships with its falsifier.
The claim and the program that would refute it are published together. Believing a page
never requires trusting its author — re-run the check and watch it pass, or fail.
-
Every check is proven able to fail.
Before a green counts, the same check runs on a deliberately broken copy of the program
and must go red — then green again on the clean one. A check that cannot fail
proves nothing.
-
REFUSED is an output, not a failure.
When the mathematics does not support a certificate, the verdict says so. One
reproduction below refuses a scenario because it admits more than one equilibrium
— the page states that instead of quietly picking one.
Run one now
Reproduce the number at the top of this page. Python standard library, nothing
installed, no network and no model — about 30 seconds.
git clone --depth 1 https://github.com/carlostoledo1891/mfg-lab
cd mfg-lab/technical-reports/bench
python3 sensitivity.py
That prints the mutation table for all 164 HumanEval items and the 1.9% of
them that cannot tell the reference solution from a broken one. verifier_audit.py
beside it reproduces the three-direction table. falsepass.py is there too and
will refuse — the wrong-answer candidates it scores are deliberately not
published, because several hundred of them are solutions engineered to pass HumanEval while
being wrong, and putting those on the internet would contaminate a benchmark other people
still use. A refusal is an output here, so it says so and stops.
Or watch a verdict flip. Node only, nothing installed — one run says CERTIFIED, the
planted mutant says REFUSED, in about a minute.
cd ../alien-science
node dual-client.js --fixture heldout-ccs-es
node dual-client.js --fixture heldout-ccs-es --plant-mutant
The last command breaks the program on purpose. Compare the
verdict field between the two runs: CERTIFIED becomes
REFUSED, and the headline goes from high PGR + CERTIFIED fragment to
high PGR + REFUSED. That flip is the point — it is the proof that the first
answer could have come out differently. Read the verdict, not the outer
status: the run as a whole reports REFUSED either way, because
the pack withholds a scenario it cannot certify, and that is the correct answer both
times.
For the record: six shipping cases, dated — errors found in this
site’s own published work, none reported by a reader first. Five are in the
errata log with their witness, their fix, and a control that now
goes red. The sixth is still open: a fix that was real, silently un-done by an
unrelated improvement, caught only because the instrument was run by hand. It stays on
the page until it closes — nothing here is quietly corrected.
Where this work has gone, and what has come back
More
Everything else, including the pages this list leaves out, is under
Reports.