A report headed “25 of 25 proofs verified” sounds conclusive. It is only as strong as the comparisons underneath it.
The recovered House ASI testing review identified self-comparisons, shared solver formulas, and a budget check whose tolerance allowed an overrun to pass. These are valuable findings because they show how a polished evidence format can carry weak evidence.
Separate a record from a proof
A structured check can record left-hand value, right-hand value, tolerance, residual, and outcome. That is useful instrumentation.
It becomes meaningful validation only when the expected value and acceptance rule can expose a relevant error.
Comparing a variable with itself establishes no independent correctness. Logging a count is an observation, not a proof that the count is right.
Use a reference with a different failure path
If the solver and verifier share the same formula and implementation, they can share the same mistake.
Use an authoritative known result, a separately implemented method, an invariant that is independently justified, or a carefully designed combination. Independence is not achieved merely by copying the code into another file.
Check a range of inputs, including cases the routine was not written around. Record the domain where the method is valid.
Match the check to the requirement
A maximum budget is a one-sided constraint. If a hypothetical operation needs 4,620.92 units and the budget is 4,200, the overrun is 420.92. A large symmetric tolerance around the budget does not turn that into compliance.
The archive’s orbital example reported those values in meters per second and still passed because the tolerance was too broad. The lesson is about test semantics: “close to a target” and “no greater than a limit” are different requirements.
Name which one the check implements.
Explain numerical tolerance
Tolerance should reflect the calculation, reference precision, scale, and intended use. A convenient value chosen to make a test pass is not an error model.
Use absolute and relative tolerances deliberately. Inspect values near zero, large values, and cases near an acceptance boundary.
A residual close to floating-point precision can be expected for an algebraic identity. It does not automatically demonstrate extraordinary physical accuracy.
Keep system quality separate
A numerical solver test, an orchestration test, and a benchmark of reasoning quality answer different questions.
Do not place scores from different rubrics on one improvement trajectory. A pipeline’s internal selection score is not directly comparable to accuracy on another task set.
Report denominators and failure types. Include invalid outputs, timeouts, unavailable references, and checks that were skipped.
Challenge the checker with plausible wrong answers
OpenAI’s July 2026 coding-evaluation audit documents how tests can be incomplete or inconsistent with the intended task. A useful response is to test the evaluator’s ability to reject known defects before trusting a clean score.
For the budget example, include an amount just below the limit, exactly at the limit, and just above it. Also test missing units, non-finite values, and a negative amount where the domain forbids one. An over-limit value must fail the maximum constraint even when it is numerically close.
Use property-based testing tools such as fast-check to generate cases and reduce failures to small examples. The property must come from the requirement: adding a positive cost cannot turn an already excessive total into a compliant one.
Distinguish executable checks from formal proof
Lean’s elaboration and compilation reference describes a kernel that checks proof terms after elaboration. That provides a different kind of assurance from matching a calculated number or asking a language model whether an argument sounds correct.
Even a kernel-checked theorem establishes the formal statement under its assumptions. Review whether that statement expresses the intended real-world requirement and whether its assumptions are justified.
Label evidence accordingly: numerical comparison, invariant test, independent recomputation, rubric assessment, or formal proof. Keep skipped checks and unavailable references visible. A collection containing several kinds of checks can be useful, but calling every successful row a proof makes the evidence harder to interpret.
These additions propose a stronger validation process. The archive’s 25-of-25 headline remains a historical claim with the weaknesses described above.
Rebuild the evidence packet
A useful packet contains the input, implementation revision, reference source, acceptance rule, raw output, residual, and final status.
It should let another person reproduce the result and disagree with the interpretation if necessary.
The immediate objective is not a perfect-looking score. It is a test suite whose failures are informative and whose successes support exactly the claims being made.
Keep a good idea close.
Follow Signal Tower
