On 6 November 2026, the public Research Artifact Ledger recorded three third-party reports of Comparator replay for OpenAI Math’s GaussianMoat challenge at the exact source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. The records concern the same encoded endpoint, OAI.GaussianMoat.fullMain.
The Toledo cert-machine record reports Comparator exit 0 and acceptance by Lean’s default kernel and stock nanoda. The MathVet status row records a sandboxed pass for the named theorem at the same pin. The Reilly corpus row records ACCEPT_BOTH, with Lean and nanoda accepting and exit 0.
Together, these are three publicly inspectable records of replay acceptance for the encoded endpoint at one pinned source revision. They are not three independent mathematical proof audits, and the records may derive from overlapping challenge runs. The published update does not establish that the Lean declaration corresponds to every statement in the associated paper, that every imported proof is correct, or that cached dependencies match their source code.
The local project’s Comparator harness was not run for this update. The third-party reports add external replay evidence; they do not change the local run history or establish full theorem correctness, cache-to-source authentication, or theorem-wide assurance. Those questions remain open in the Ledger’s pinned update.
No published comments yet.