Machine verification of the fixed r = 5 case of Erdős Problem 617

Independent machine verification of the fixed r = 5 case of Erdős Problem 617 (an Erdős–Gyárfás balanced-colouring conjecture): every five-colouring of the unordered edges of K₂₆ has a six-vertex set on which some colour is absent. With the standard affine lower bound on K₂₅ this gives the set-colouring Ramsey identity R(6;5,4) = 26. The original mathematical proof is due to Robert Sneiderman (github.com/Robby955/erdos-617-fixed-cases, pinned commit 735c2eeffcb5c8abe92f8a6be04be2fa3c8bb6ab). This record archives the verification: the full argument is a theorem in Lean 4 (v4.32.0, mathlib revision 81a5d257c8e410db227a6665ed08f64fea08e997). The exported declaration is e058Problem617AtFive : Problem617At 5, and its assumption audit reports exactly propext, Classical.choice, and Quot.sound. The finite special-Brooks obstruction is discharged by 89 RUP-only LRAT certificates, each accepted by two independent external checkers and replayed inside the Lean kernel, with a kernel-checked semantic and symmetry bridge back to the colouring statement, so no solver output is a trusted premise. Files: the five artifacts are the byte-exact assets of the repository's frozen e058-r5 publication release. erdos617-r5-formal-verification.pdf is the preprint (390,401 bytes, SHA-256 c248918bde85c9a0306c13e751b613760be88f02b9474b1565af8662a1d5a543). The three .tar.xz archives contain the pinned source, the 89 compressed CNF/LRAT certificates, and the audit evidence; SHA256SUMS authenticates all four payloads, so the record is self-verifying via sha256sum --check SHA256SUMS. The repository's main branch carries a later wording-only revision of the preprint (SHA-256 fbcd4e1b…; no mathematical, numerical, attribution, or scope change); this record intentionally preserves the frozen snapshot. Scope and status: this verifies the fixed r = 5 case only; the conjecture for all r ≥ 3 remains open. The project was substantially AI-assisted (full disclosure in the PDF and in AI_USAGE.md inside the source archive); it has not yet received independent expert review. A clean-mirror replay of the complete audit, kernel imports included, takes about seven hours on ordinary hardware; the replay guide is REPRODUCE_E058.md in the source archive. Repository: https://github.com/RamazanKara/erdos-617-r5-formal-verification