Where things stand

Status (T119, Oct 2026): 0 of 154 statements settled. Every attempt so far is a dead end, and every audited statement is faithful, with no junk-value edge case. Audited and faithful: 1065.i/ii (N3,N4,N5,N12,N18), 1068, 1075 (N27), 108 (N31), 1082.i (N32), 11 and all its variants (N56,N57,N58,N62), 1158 (N63), 317.claim2 (N53), 699 and szekeres_strengthening (N54), 931.exists_prime (N55), 65.ii (N51), and the Ramsey/design batch in N47 (551, 556, 159, 552, 87, 1029, 1030, 544, 566, 568, 665, 734, 719, 836.ii, 89, 653, 81, 1035, 1159, 982, 86, 386, 849). T119 added (chat): HasMonotoneAP for 196/197 allows decreasing APs (List.IsAPOfLengthWith has a .reverse disjunct, so the earlier chat claim that only increasing APs count is wrong). StrictCoveringSystem for 7 and 273 has a Fintype index and injective moduli. chromaticCardinal uses colour types in the same universe as V, so 1175 and its variants and 1176/1177 have no universe junk. Nat.Full makes 0 k-full, but this changes nothing in 364, 137, 938, 940, 943 or 913. In 288 the intervals may overlap or repeat, but only 7 integer pairs exist with endpoints ≤80. Search data (no counterexamples): the 11 variants to $2\cdot {10}^7$ (N58). 699 to 120000; the strict variant has sporadic exceptions in the family $n=3^k+1$ (k=1,3,5,7,13) and at $n=2^k$ (N54). 931.exists_prime to $2\cdot {10}^{11}$ (N55). 686.four/25 and 488 (chat). 65.ii annealing for n≤10 (N51). Lesson: edge-case disproofs are basically exhausted for the audited ~60 statements. What remains is (a) existential statements where one explicit object settles everything, checkable by decide/norm_num, and (b) small Lean-friendly families. Best untried existential targets: 366 (∃ n>0 with n 2-full and n+1 3-full), 850 (x≠y with equal radicals at x, x+1, x+2), 137 (a product of ≥3 consecutive integers that is powerful), 203 (a 2D Sierpiński-type covering), and 723.eq_12 (projective plane of order 12, infeasible). Universal statements with only a far-out counterexample (11, 699, 931, 985, 389) look exhausted at lab-scale compute.