TradingCalc
FROM THE BLOG · BENCHMARK · VERIFICATION

Two checkers said yes. The proof was false.

A checker is a program whose job is to say whether an answer is right: a proof checker in mathematics, the reference answers of a benchmark, a test suite that goes green. On 25 July 2026 the best known proof checker, Lean, accepted a claimed disproof of the Collatz conjecture that was not one, and a second checker, written separately to catch exactly this, accepted it too. I could not pass this by, because my own benchmark has the same weak spot. So here is the story, then what I found in my answer key.

OPEN THE BENCHMARKRAW DATA
0125 JULY

A disproof that passed both checkers

Lean is a program that checks mathematical proofs. You write a proof as code, Lean says yes or no, and a yes means nobody has to read the steps. That is why AI labs like it: a model can produce pages of proof in minutes and a machine can say whether it holds.

On 25 July a developer, Ramana Kumar, published a project that claimed to disprove the Collatz conjecture, made with AI help. Lean said yes. A week-old version of nanoda, an independent checker written in Rust that exists so that one Lean bug does not decide everything, said yes as well. The conjecture is still open, I should add. Nobody told it.

On 28 July Kiran Gopinathan boiled the repository down to a small proof of False and opened issue 14576. The cause was a bug in how Lean's kernel handles nested inductive types, reachable only by sending a declaration straight to the kernel and skipping the part of Lean that normally catches it. The fix was pushed about an hour after the report. nanoda had its own, different bug (it did not check the type name in a projection node), reported and fixed a week earlier, which is why it was the week-old version that said yes. Leonardo de Moura, who made Lean, wrote it up in a postmortem and calls it an implementation bug, not a hole in Lean's meta-theory.

My two cents: this is not a story about Lean being bad. A fix in an hour and a public postmortem is how it should go. What stays with me is smaller. Two checkers, written by different people, still had one bug each, and one bug each was enough.

02THE PHYSICS TESTS

Most of the wrong answers were not wrong

The second story is quieter and I like it more. A physics benchmark works the way mine does: a hard question, a reference answer, a count of the matches. A group of 51 authors took the answers that frontier models had marked wrong on six public physics benchmarks and had faculty and graduate researchers read each one against the question and the reference solution.

They audited 308 answers. Nineteen were real mistakes of the model. In 194 the benchmark itself was at fault, with a wrong reference solution, a missing assumption or a question that could be read two ways. In 95 the automatic grader marked a correct answer as wrong (the paper gives no grader count for two of the six benchmarks). That is 289 of 308, about nine in ten, and I should say what it is nine in ten of: the answers they audited, not all physics problems. A number like this tends to lose its denominator on the way to a headline.

The scores moved a lot after the repair. GPT-5.6-Sol went from 13% to 94.6% on one of them, PRISM-Physics, though on the questions that were kept after repair, so it is not the same test. The preprint says this itself, so read it before you quote a number from it, me included. My two cents: a leaderboard figure tells you about the test as much as about the model.

03MY TURN

My benchmark has the same weak spot

My benchmark asks 6 models 21 kinds of trading-maths questions, 105 per model, 630 answers in all: option prices, position sizes, liquidation prices, statistics on a series of returns. 613 of the 630were right. The reference answers come from the same functions that the MCP tools run, which is convenient and is also the problem. If one of those formulas were wrong, the key would be wrong in the same way. A model that happened to get it right would be marked wrong, and I would write down “the model made a mistake” with full confidence. Nice.

So I took the 7 question types that had wrong answers and recomputed their 35 reference answers from the text of the question, in plain Python that calls none of the TradingCalc code. 35 of 35 agreed. Then I read all 17 wrong replies in full to see whether any came from a question that could be read two ways. None did. The causes were these:

So the physics story does not carry over to this run. There the tests were wrong. Here the models were wrong, and in a narrow way: long hand arithmetic, and the direction of an inverse contract.

04TWO OF THE 17

A short that lost, and a liquidation below the entry

Both cases come from a smaller model and are on an inverse contract, where the size is in dollar contracts and the profit is in coins. The first asks for the result of a short that was closed higher than it was opened.

short, inverse, with fees
short 103,000 contracts at 49553.7
closed at 55827.2, fee 0.055% on both fills
 
price move = 103000 x (1/55827.2 - 1/49553.7)
           = -0.23357 BTC
fees       = 0.00055 x (103000/49553.7 + 103000/55827.2)
           =  0.00216 BTC
PnL        = -0.23573 BTC
 
the price rose, so the short lost
the model said +0.2315 BTC

The model reported a profit for a short whose price went up, and it put 72 out of 100 on that answer. The second case is a liquidation price.

liquidation of a short
short from 115273.7, 3x, maintenance margin 1%
 
margin + PnL = maintenance margin
1/3 + (E/L - 1) = 0.01    (in units of N/E)
E / L = 1 + 0.01 - 1/3 = 0.67667
L = 115273.7 / 0.67667
  = 170355.22
 
the model said 87108.6
the long-side formula gives E / (1 + 1/3 - 0.01) = 87108.59

A short is liquidated when the price rises, so the answer has to sit above the entry. The model gave a price far below it. Its working used the PnL of a long inside a short's margin condition, and that lands exactly on the long-side formula. It put 85 out of 100 on the answer. Of the 17 wrong answers, 12 came with a stated confidence of 80 or more, so a rule that says “check only when the model is unsure” would let most of them through.

05LIMITS

What my check does not cover

06CHECK IT YOURSELF

Both cases in a few lines

The snippet needs only Node. The complete recompute of the 35 references is audit-references.py, and the questions, the key and every full reply are in the raw data file.

node · independent check
// a short on an inverse contract, size in USD contracts, PnL in BTC
const N = 103000, entry = 49553.7, exit = 55827.2, fee = 0.00055;
const move = N * (1 / exit - 1 / entry);
const fees = fee * (N / entry + N / exit);
console.log((move - fees).toFixed(5));
// -0.23573
 
// liquidation of a short, 3x, maintenance margin 1%
const E = 115273.7, lev = 3, mm = 0.01;
console.log((E / (1 + mm - 1 / lev)).toFixed(2));
// 170355.22

I have no way to check the checker all the way down, and I doubt anyone has. What I have is a second calculation, a script and a data file that anyone can open. If a reference answer of mine disagrees with yours, I want to know about it. The full results by model and question type are on the benchmark page, and the same two calculations run as the liquidation calculator and as MCP tools, whose answers are signed so that you can confirm where they came from.

OPEN THE BENCHMARKUSE VIA MCP