15 Sep 2026
Why the model never writes the theorem.
Most formal-reasoning benchmarks check whether a model's file compiles. That leaves the model free to change the question. The single design decision that closes that hole, and why it matters more than anything else in the harness.