DISPROVED (LEAN). The site credits the disproof to Larsen using Claude Opus 4.5; Larsen's thread posts describe a multi-agent system of Claude and Gemini agents (Claude 4.5 and Gemini 3 Pro in his 2026 preprint), which produced the Lean proof and its write-up, posted in January 2026: a small modification of the construction of [ErNa89] gives a basis of order two whose representation counts tend to infinity but which is not a union of two disjoint bases of order two. The label's Lean qualifier refers to Larsen's Lean proof as posted on the thread; a later revision of it is kept in Boris Alexeev's lean-proofs repository, and this corpus has built or audited neither. The accepted claim is Larsen.