Four Colors: a First Theorem in the Mixed Degree-{3,4} Case
Formal verification · graph coloringA kernel-checked theorem: every graph with degrees in {3,4} and at most two degree-3 vertices admits a strong majority 4-coloring — the first unconditional mixed-class bound of four, where the best published bound was five. The general mixed case and the full four-color conjecture remain open.
11 July 2026Strong Majority Edge-Coloring
Formal verification · graph coloringA Lean-verified alternative proof that five colors suffice for every admissible graph — posted 30 June, kernel-checked 11 July. The conjectured four-color bound remains open.
July 2026A Pattern-Avoidance Conjecture, Proved in Lean 4
Formal verification · enumerative combinatoricsThe {1132, 3312} conjecture of Elizalde & Luo, proved for all n and kernel-checked in Lean 4 — a positive result from the feasibility study.
12 June 2026C(13) ≥ 36 record
Numerical record · discrete geometryAn explicit 36-point certificate raises the recorded lower bound for the “no 5 on a sphere” grid problem without claiming C(13) = 36.
11 June 2026Borsuk Conjecture 3
Formal verification · discrete geometryA four-point witness in dimension 2 refutes the printed biconditional in Lean 4; the unstated full-set variant remains open here.
12 June 2026Sun Conjecture 4.6
Exact computation · number theoryBoth sign clauses in part (ii) fail as stated at p = 29, while the divisibility assertion in part (i) is not refuted.
June 2026Graffiti 143 & 154
Exact computation · spectral graph theoryExact witnesses refute 143 under both average-distance conventions and 154 under the standard-deviation reading.
June–July 2026Thirteen Verified Results
Feasibility studyThirteen mechanically checked results: eleven refutations of conjectures as stated, one Lean proof, and one numerical record.