---

Claim. The statement of [[problems/discrete_geometry/E0846/_index|Problem 846]] is false: there is an infinite $A \subset \mathbb{R}^2$ and an $\epsilon > 0$ such that every $n$-point subset of $A$ contains at least $\epsilon n$ points with no three on a line, while $A$ is not a finite union of sets with no three on a line. The Lean theorem erdos_846 in the formal-conjectures repository proves answer(False) for the problem's formal statement, with the definitions of the statement file: a set is $\epsilon$-non-trilinear when every finite subset $B$ has a collinear-free subset of size at least $\epsilon |B|$, and weakly non-trilinear when it is a finite union of collinear-free sets. The argument, as summarized on the site's forum: label the vertices of the infinite complete graph by a rapidly growing sequence $x_1, x_2, \ldots$ and place one point $(x_i + x_j,\, x_i^2 + x_i x_j + x_j^2)$ for each edge; three points are collinear exactly when their edges form a triangle; a graph with $n$ edges has a bipartite subgraph with at least $n/2$ edges, so $\epsilon = 1/2$ works; and by the infinite Ramsey theorem every finite coloring of the edges has a monochromatic triangle, so no finite union of collinear-free sets covers the points.

Source. DeepMind reports, in a post of 2026-02-25 on the site's forum, that a DeepMind prover agent found the proof on 2026-02-21 without human guidance beyond the formal statement from formal-conjectures, and that the file compiles with Lean 4.22. The announcement was posted for DeepMind by a member of its team, George Tsoukalas, whom the Lean copy linked above lists as a formal author beside the agent; the organization is taken as the claimant, following the site's credit, and the agent is the system the post names. The proof is the formal-conjectures file at the commit of 2026-02-25 linked above (the file at main has since reverted to the statement with sorry, carrying a formal_proof attribute that points at that commit); a copy, whose header names the agent as informal author and the agent and Tsoukalas as formal authors, is in a public repository of Lean proofs of Erdős problems. The construction is the one of Putterman, Sawhney and Valiant, found independently. Both results were announced on the site's forum on 2026-02-25, DeepMind's first, Putterman, Sawhney and Valiant's later the same day with a hosted copy of their paper, whose arXiv submission is stamped 2026-02-24.

Acceptance. The site's curator, T. F. Bloom, marks the problem disproved and credits DeepMind with an independent disproof on the problem's page at erdosproblems.com (page last edited 2026-04-10, read 2026-10-07); that credit is the reviewed evidence. The Lean proof is third-party Lean that this corpus has not built or audited, so the claim is not formalized here, and there is no refereed write-up.