Independently checked AI-led

Erdős Problem 654 answered negatively by Google DeepMind's Aletheia agent

An agent built on Gemini Deep Think produced an elementary counterexample showing that $n$ points in the plane with no four on a circle need not contain any point having $(1 - o(1))n$ distinct distances to the others, a negative answer to Erdős Problem 654 as the problem database formulates it; a third party has since proved that negative answer in Lean, from a different construction.

Lab: Google DeepMind
Model: Aletheia, a mathematics research agent built on Gemini Deep Think
Field: Mathematics
Date: 2026-01-29
Human collaborators: Tony Feng, Trieu Trinh, Garrett Bingham, Quoc V. Le, Thang Luong
Problem posed: 1997 · open 29 yrs

Sources

Original work

arXivSemi-Autonomous Mathematics Discovery with Gemini, A Case Study on the Erdős Problems↗GitHubveljjanoski/erdos654-palomar at the registered commit↗

Independent commentary

erdosproblems.comProblem 654, recording the disproof of the strongest form↗

What was found

Write $f(n)$ for the largest number such that every set of $n$ points in $\mathbb{R}^2$ with no four on a circle contains a point at $f(n)$ or more distinct distances from the rest. Erdős asked in his 1997 problem collection whether $f(n) > (1 - o(1))n$ , the trivial bound being $f(n) \ge (n - 1)/3$ . Aletheia answered no: its counterexample places $2m$ points on each coordinate axis, at powers of 2 and 3, giving $4m$ points in which every point sees at most roughly $3n/4$ distinct distances. The paper reports 13 problems marked open in the database addressed by the agent, some by novel solutions and some by locating solutions already in the literature, and its Table 1 classifies this one as a Partial AI Solution, meaning the problem carried several questions and the agent solved the first of them. An independent Lean 4 development by Daniel Veljjanoski, registered at Palomar on 2026-11-02, proves both the negative answer and the quantitative form, using a different set on the same two axes, the points $(\pm 2i, 0)$ and $(0, \pm(2j - 1))$ for $1 \le i, j \le m$ , and finishing the no-four-concyclic condition by parity rather than by unique factorization.

Novelty check

The problem database at erdosproblems.com/654 records this work as disproving the strongest form of the conjecture, so an independent maintainer has accepted it against the problem as stated; the page was last edited 2026-02-01 and thanks the Superhuman Reasoning team at Google DeepMind. The paper itself reports no prior solution and the Palomar record cites only Erdős's own 1997 collection as the source of the question. Nothing in this registry covered it: no entry names Aletheia or this problem, and the nearest neighbours are 2025-10-19-gpt5-erdos-retrieval, which is retrieval rather than a new result, and the Lean-formalized Erdős entries 2026-08-19-erdos-501-independence, 2026-09-26-erdos-1220-not-provable, 2026-10-19-erdos-173-monochromatic-triangles, 2026-10-19-erdos-111-bipartization and 2026-10-19-erdos-408-iterated-totient. The paper was posted in January 2026 and reached this registry only on 2026-11-02, surfaced by the watch run through the Palomar registration of a formalization that cites the construction, because the disclosure sits in the paper's body rather than its abstract.

Caveats and known objections

Graded independent rather than formal, on the precedent of 2026-05-erdos-unit-distance: a registration does not by itself move a grade, and the registered Lean proof deliberately uses a different point set from the paper's, as Palomar's own abstract for the record states. What is machine-checked is therefore that the statement Erdős asked about is false, not that Aletheia's construction works; the construction the agent actually produced has never been formalized, and no kernel has looked at it. The grade rests instead on two parties outside Google DeepMind having engaged with the result: the maintainer of the problem database recorded it as disproving the strongest form of the conjecture, and an independent Lean development reached the same negative answer by another route. Both of those are thinner than the word independent usually implies, and the entry should move to formal only if someone formalizes the paper's own construction. The statements in that development's Challenge.lean are copied verbatim from google-deepmind/formal-conjectures, so the statement of record comes from the same laboratory that produced the result, and nobody independent of it is on record as having audited that the Lean statement is what Erdős asked. Palomar records trust level high with two kernels, nanoda and con-ron, and permitted axioms exactly propext, Quot.sound and Classical.choice, but its own review outcome is neutral and its reviewer is a model rather than a human referee, and the repository's formalization.yaml records review as self-assessed with no reviewers. The Lean proofs were written by Claude Opus 5.5 under Veljjanoski's direction, so the formalization is itself largely machine-generated. On the mathematics, the paper is explicit that this addresses only part of the question: the counterexample puts every point on the union of two lines, so it says nothing about the strengthening in which the points are in general position, a limit the database page states as well, and the authors write that they consider the solution to address only a part of the question even though it fully addresses the formulation on the database at the time of writing. Aletheia also answered the variant assuming no three points collinear, and that answer was incorrect, so the authors omitted it. The paper's own bookkeeping is inconsistent: the arXiv listing abstract counts 5 novel autonomous solutions against 8 from the literature while the version 3 full text counts 4 against 9, and section 1.2 lists this problem among the autonomous solutions while Table 1 classifies it as partial, so no headline count from this paper should be quoted without saying which version it came from. The paper is on arXiv only, with no journal reference and a CC BY-NC-ND licence, so it has had no peer review. Autonomy is ai-led rather than autonomous: the humans assembled the problem list, and the paper states that the solutions it presents are human-rewritten versions of the agent's raw outputs.

Independent checks

Thomas F. Bloom, maintainer of erdosproblems.com: Records on the problem page that the strongest form of the conjecture was disproved by Aletheia, which constructed a set of $n$ points in $\mathbb{R}^2$ , no four on a circle, with at most $3n/4$ distinct distances from any single point, while noting that the construction places all points on the union of two lines and so does not bear on the stronger version with the points in general position. · link ↗

Daniel Veljjanoski (Lean 4 development registered at Palomar): Proved the negative answer and the quantitative form in Lean 4 against Mathlib, confirming by an independent route that the statement is false, but using a different point set from the paper's, so the check does not reach Aletheia's construction. The Lean proofs were machine-generated under his direction and the repository records review as self-assessed with no reviewers, so this confirms the mathematics rather than the paper. · link ↗

Machine-checked elsewhere

PalomarErdős Problem 654: distinct distances from a point when no four points are concyclic

PALOMAR-2026-11-02-000006 · veljjanoski/erdos654-palomar at fd7a8dc3cf52 · checked 2026-11-02

ProvedErdos654.erdos_654.parts.iErdos654.erdos_654.variants.feng

A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.

Permitted axioms are exactly propext, Quot.sound and Classical.choice, with two kernels, nanoda and con-ron, and trust level high. The proof uses a different point set from the one in the paper, so it certifies the negative answer rather than Aletheia's construction.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

Entry history (1 event)

2026-11-02AddedEntered the registry graded Independently checked and AI-led.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Graded independently checked for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Erdős Problem 654 answered negatively by Google DeepMind's Aletheia agent. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-01-29-erdos-654-distinct-distances

BibTeX

@misc{whataifound-googledeepmind-2026-distances,
  title        = {Erdős Problem 654 answered negatively by Google DeepMind's Aletheia agent},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Google DeepMind. Verification: Independently checked. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-01-29-erdos-654-distinct-distances}
}

Related findings

Formally verifiedErdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateralPlasma AI · 2026-10-19 Formally verifiedMeasurably isomorphic Bernoulli shifts with different base entropies, proved in LeanIndependent · 2026-10-27 Formally verifiedErdős Problem 408: an unconditional normal order for the number of totient iterationsPlasma AI · 2026-10-19

combinatorics discrete-geometry distinct-distances erdos-problems lean formalization construction

← All mathematics findings in the registry