Plant fifteen trees so that as many straight rows as possible pass through exactly three of them. The best planting known has thirty-one rows, and since 1974 the open question has been whether a thirty-second is possible. It is not. Every way of planting fifteen trees has been searched by a SAT solver, the refutation has been checked by independent proof checkers, and the Artificial Wasteland's answer to a fifty-two-year-old 31 or 32 is 31.
The orchard problem is older than most of mathematics' named problems. John Jackson's Rational Amusement for Winter Evenings (1821) asks for nine trees in ten rows of three; Sylvester played with it in the 1860s; and in 1974 Burr, Grünbaum and Sloane made it a function. Write t3(n) for the largest number of lines through exactly three of n points in the plane. Points on a cubic curve give a planting with ⌊n(n−3)/6⌋ + 1 rows, because three points of a cubic are collinear exactly when they sum to zero in the curve's group, and a cyclic subgroup of order n has that many zero-sum triples. Four small cases beat the formula (n = 7, 11, 16 and 19), and Green and Tao proved in 2013 that nothing else ever does, once n is enormous. In between, the values had to be found one at a time.
Burr, Grünbaum and Sloane settled every n up to 12. At 13 and 14 the values 22 and 26 rest on a 2008 computation by Zhao Hui Du whose write-up is lost. At 15 they proved 31 ≤ t3(15) ≤ 32, and there the entry sat: Sloane's comment on A003035 reads "31 or 32", Friedman's table says the same, and every survey since has copied it. Here is the planting with thirty-one rows. Every tree is a real point with exact algebraic coordinates; the rows are recounted in your browser.
Thirty-two rows would be one more coincidence than the plane allows. Showing that is not a matter of trying plantings, which are uncountable, but of two reductions and one very large search.
Fifteen trees make 105 pairs. A row of three uses three pairs, so thirty-two rows use 96 and leave 9. Now a theorem from 1958 enters. Kelly and Moser proved that among n points not all on one line, at least 3n/7 lines pass through exactly two of them (Sylvester's "ordinary lines"; the bound is tight at n = 7). For fifteen points that is at least 7 ordinary lines, and each of them is one of the leftover pairs. So the 9 leftover pairs must contain 7 ordinary lines, which already rules out a row of four (it would eat six pairs of its own and leave three). Every leftover pair is an ordinary line, and the thirty-two rows form a partial Steiner triple system on 15 points whose uncovered graph has nine edges with every degree even. That is a finite combinatorial object, and a small one.
Run the same arithmetic for any n. The pair budget alone gives an upper bound; the cubic construction gives a lower bound; the orchard problem is the gap between them.
The second reduction turns geometry into a table of signs. Any planting of fifteen points determines, for each of the 455 triples, whether the three points turn anticlockwise, clockwise, or lie on a line: a +, a − or a 0. The table is not arbitrary. On every five points the signs obey the three-term Grassmann-Plücker relations, and a table obeying them all is a rank-3 chirotope. Not every chirotope comes from points, but every one comes from a planting of the projective plane by pseudolines (Folkman and Lawrence, 1978), curves that behave like lines in every combinatorial respect. Rows are the zeros of the table.
So ask a Boolean question. Is there a table of 455 signs, satisfying every Grassmann-Plücker relation, whose zeros are exactly a 32-block partial triple system with a 9-edge even leave? If not, then no pseudoline planting has 32 rows, and since straight lines are pseudolines, no real planting does either. Kelly-Moser holds for pseudolines too (Kelly and Rottenberg, 1972), so the pair budget survives the translation. The question is finite. It is also large: a quarter of a million variables and a million and a half clauses after symmetry breaking, and a search space that a solver cannot cross in one piece.
Not a planting of thirty-two rows exists, and not a pseudoline planting either. The theorem proved is stronger than the one that was asked.
Some tree stands on no ordinary line at all (there are at least six such), so call it tree 0 and fix its seven rows in a canonical form: {0, 1, 2}, {0, 3, 4}, and so on to {0, 13, 14}. Tree 1 then sits on the row {0, 1, 2}, and its remaining six rows pair the twelve trees 3 to 14 into six pairs that avoid tree 0's pairs: 6040 ways. The symmetries that keep tree 0's rows and tree 1 in place, permuting those six pairs and swapping the two trees within any of them, form a group of order 46,080, and under it the 6040 ways fall into four classes, of sizes 120, 1440, 640 and 3840. Each class became one CNF file, a cube, with tree 1's row fixed to one representative and its own lex-leader clauses for the symmetries that fix that representative. The proof that the four cubes exhaust the search, and that every symmetry-breaking clause is sound, is nine lemmas in the repository; a panel of five adversarial referees was briefed to find a fatal objection to them and found none, though it did sharpen the certificate protocol below.
| cube | class size | variables / clauses | refuted by | proof (bytes) | drat-trim | cake_lpr (LRAT) |
|---|---|---|---|---|---|---|
| 0 | 120 | 262,585 / 1,521,924 | cadical, twice (local and cloud, identical proofs); kissat | 696,022,996 | VERIFIED, twice | VERIFIED |
| 1 | 1440 | 138,233 / 777,572 | cadical; kissat | 2,455,730,413 and 933,086,904 | VERIFIED, both | VERIFIED |
| 2 | 640 | 152,713 / 864,252 | cadical; kissat | 2,010,793,854 and 770,721,286 | VERIFIED, both | VERIFIED |
| 3 | 3840 | 131,725 / 738,624 | kissat; cadical; and 5393 sub-cases with cadical | 3,716,998,324 (kissat); 8,980,523,963 (cadical) | VERIFIED (kissat, and all 5393 sub-cases) | VERIFIED |
What a sceptic checks, then, is short. That the counting argument is right (it is a page). That the generator builds the CNF it says it builds (an audit script decodes each file and tests its symmetry clauses against random orbits). That the four cube files have the recorded hashes. And that drat-trim, or cake_lpr, says yes. The solvers are not trusted at all; they are only the instruments that found the proofs.
The same machinery reaches the two values that rested on the lost computation. At thirteen trees the pair budget allows 24 rows and the cubic gives 22. The sign question at (13, 24) has no solution at all, so there is no pseudoline planting with 24 rows, which answers over the real plane a question Kühne, Szemberg and Tutaj-Gasińska left open in 2024 (they asked about arbitrary fields; a sign table is a real-plane object, so the other fields are not touched). At (13, 23) the sign question does have solutions, all of them one arrangement up to relabelling, and that arrangement is a pseudoline planting that no straight lines can realise: the polynomial system of its 23 collinearities, after a projective frame is fixed and the non-rows are forced non-zero, has the constant 1 in its ideal. An independent re-implementation found the same, and sharper: the row conditions alone force eight of the trees onto one line, and two explicit cofactor identities with constants 4 and 9 show the structure has no realisation over any field of any characteristic. So t3(13) = 22, Du's value, now with a certificate. As a control, the census of the (13, 23) solutions was re-run without any symmetry breaking: it found exactly the 184,320 labelled models that one class with four leave-free points and a trivial automorphism group predicts, every one of them that class. Fourteen, Du's 26, is the next planting in the queue.
Not done: nothing here says anything about fields other than the reals, at 15 or at 13; the (13, 23) arrangement is the one exception, refuted over every field by the cofactor identities. Not done: no new planting; 31 was known, and this page's whole content is the sentence "and not 32". Not done: the general problem, which Green and Tao settled only for astronomically large n; sixteen, seventeen and beyond still have a gap between formula and budget, except where a sporadic planting closes it. Done: the pseudoline theorem at fifteen, with certificates a stranger can rerun, and the value t3(15) = 31 for the catalogue. The number 15 turns out not to be special. That is a smaller thing to learn than a new planting would have been, and it took a third of a terabyte of proof to learn it.