Claude Code Solves the Orchard Problem

Claude Code determined that the maximum number of lines for the 'Orchard Problem' regarding 15 points, which had remained unsolved since 1974, is 31. This case demonstrates the resolution of a geometric puzzle that had been debated for 52 years through AI agent collaboration.

Proof Process and Verification

• Problem Definition: The problem involves finding the maximum number of lines that pass through exactly three points when arranging n points on a plane. For 15 points, it was previously estimated that either 31 or 32 lines were possible, but this study proved that 32 is impossible and the maximum is 31.
• AI Utilization: Claude Code oversaw the research and distributed tasks to multiple agents. It reduced the geometric conditions to four finite SAT (Satisfiability) instances and independently refuted them.
• Verification Reliability: The proof generated by the SAT solver was checked by drat-trim, converted to LRAT format, and finally approved by the formally verified cake_lpr checker in HOL4. This eliminated the possibility of errors in the SAT solver itself.

Significance

Beyond simple line arrangements, this result demonstrates that 32 lines are also impossible in pseudoline arrangements. The author stated that this is part of a public project using Claude Code to systematically solve and verify mathematical problems.