Carlos Toledo
Research notes · Campinas, Brazil · UTC−3

Verification for machine-generated mathematics — and for the tests that grade it

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.

Where this work has gone, and what has come back
Stated exactly: filed is not accepted, and posted is not replied. Nothing on this site has been peer-reviewed, and no result here has yet been reproduced by anyone else — which is why every page ships the program that would refute it.

Start here — for a reviewer with ten minutes

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

How a result earns a green light

The house rule is that green proves nothing until it can go red. Three obligations, on every page here:

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

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

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

What counts as a certificate here — and what is refused: /certificates. The full toolchain, with its own code on the page: /stack.

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.

More

Everything else, including the pages this list leaves out, is under Reports.