Verification
& provenance.

What was checked

The Axiom Proofs submission workflow accepted both formalizations in its official and wide comparator lanes. These checks compare the submitted theorem with the fixed benchmark statement and check the Lean proof. The acceptance records below link to those workflow results and the preserved source artifacts.

The recorded final theorem audits list only the standard Lean dependencies propext, Classical.choice, and Quot.sound. Neither accepted proof overlay contains sorry, admit, or newly introduced axioms. The benchmark’s trusted challenge scaffold is separate from the submitted proof overlay.

This companion does not change the accepted Lean sources. Each site build verifies every copied proof file against the SHA-256 hash in its acceptance record and resolves every writeup-to-Lean link to an existing declaration. Those publishing checks preserve provenance; they do not rerun the Lean kernel. The linked comparator runs are the proof-verification evidence.

How the proofs were produced

Strong Mason. The recorded Codexiom worker used GPT-5.6 Sol Pro with an already audited AxiomMath combinatorial atlas development supplied as input. Its recorded final run audited that dependency chain, reconciled the counting and normalization conventions, and produced the benchmark adapter. It would be misleading to describe that final run as creating the whole proof from scratch.

Heron–Rota–Welsh. The proof was produced across a supervised sequence of Codexiom runs. The acceptance record credits GPT-6 Astra with the decisive incidence-form construction and final proof, building on coefficient reductions and exploratory work from earlier runs.

For both, the submission records describe human work as theorem selection, orchestration, recovery, review requirements, and acceptance criteria. The site reports that provenance without inferring independent verification of every production-history claim from a successful mathematical check.

What this site publishes

The site contains the mathematical explanations, references, and verification summaries. The new repository preserves copies of the accepted proof overlays and the sources for this writeup. It remains private within AxiomMath, as do the original source and workflow records. Following a Lean source or acceptance link therefore requires the appropriate GitHub access.

The source links use a fixed archive commit rather than a moving branch. Hashes below identify the exact accepted artifacts; the displayed file counts include all preserved supporting modules and are not claims about the size of a minimized proof.