PXP-18B537AWDH1F · Version 1

Eleven lines cannot form 33 Kobon triangles: a checked SAT proof over all pseudoline arrangements

Papex Labs

The Kobon triangle problem asks for the largest number K(n) of bounded triangular faces in an arrangement of n lines in the plane. For n = 11 the best known arrangements have 32 triangles and the classical counting bound allows 33. In October 2026 the value a(11) was removed from OEIS A006066, because the lemma that extends the counting bound to arrangements in which three or more lines meet at a point has a counterexample. We show that no arrangement of 11 pseudolines, simple or not, has 33 bounded triangles; hence K(11) = 32. A counting argument reduces every arrangement with at least n(n-2)/3 triangles to two cases: simple arrangements, and arrangements in which three concurrent lines carry three particular triangles. Each case is a SAT instance over rank-3 chirotopes. The simple case is refuted by a single LRAT proof checked with lrat-check. The other case is refuted by a cube-and-conquer tree with 67,614 leaves, each refuted by an LRAT proof that was checked as it was produced, and 1,094 splits whose covers were checked in the same way. The computation took about 2,540 CPU hours.