Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to Problem 397 is no: the equation
has infinitely many solutions in which all the indices are distinct. Neel Somani posted the family in the site's discussion thread on 11 January 2026, with a proof produced by ChatGPT (GPT-5.2 Pro, as the post states): for every integer , with ,
The verification is two lines. Write , so that . Then
and the product of the three ratios is , which equals because and . For the six indices satisfy , so they are distinct, and different values of give different solutions.
Other constructions. The thread holds more. Sharvil Kesarwani (SharkyKesa on the site) gave two two-parameter families, found by a computer search for one-parameter families (11 January 2026); the case of the first is the family above. Kesarwani then counted solutions with every index at most (12 January 2026), most of them with a different number of indices on each side, the smallest such primitive solution having indices against . Terence Tao gave an entropy argument (12 January 2026): products of central binomial coefficients over subsets of carry fewer than bits of information once is large, so two subsets must share a product. Nat Sothanaphan posted a counting version of Tao's argument and an exponential lower bound, , for the number of collisions with indices at most (13 and 14 January 2026); both came from ChatGPT, as the posts state, and Sothanaphan wrote of not having fully checked the counting rewrite. These are thread posts, not dated manuscripts, and have no page here; the site credits the disproof to Somani. A related earlier MathOverflow question (number 138209, from 2013) asked for nontrivial solutions with equal index sums, repeated indices allowed, and Noam Elkies answered it with a construction of solutions; the thread discussed whether it yields infinitely many solutions with distinct indices and left that open, so it is recorded as context and not as a claim.
Formalization. A Lean 4 file generated by Aristotle, posted as a gist on
11 January 2026 by Wu, posting as llllvvuu, as the formal-conjectures
statement file credits it, and linked above at the gist's only revision,
defines a solution as a pair of lists of indices, proves the identity above as
central_binom_identity, shows that the family is a solution for every
, and concludes infinite_solutions. The gist declares itself a
formalization of Somani's result: its description names it a formalization
of Somani and GPT-5.2 Pro's counterexample and links post 2936 of the thread,
and its header says that Aristotle generated it to formalize the provided
solution. The formal-conjectures statement file for the problem names that
gist and a proof of its own statement erdos_397 : answer(False) ↔ …Finite
in a fork of the repository, linked above at the commit the file pins, as its
formal proofs; the fork's file carries the statement file's docstring, which
credits the negative answer to Somani using ChatGPT, and names no author of
its own. Both files are therefore formalizations of this claim and neither is
an independent proof. Boris Alexeev's repository of Lean proofs carries the
gist as Erdos397.lean, linked above at a pinned commit: the file opens by
declaring itself a formalization of a solution to the problem, names GPT-5.2
Pro and Somani as its informal authors and Aristotle and Lawrence Wu as its
formal authors, cites the gist, and ports it to the repository's Mathlib.
This corpus has not built or audited any of the three files, so none is
listed as evidence.
Earlier occurrence and independent report. Feng and coauthors (arXiv:2601.22401, first posted 29 January 2026) report in Section 4.1 of their case study that their Gemini-based agent Aletheia produced the same family in December 2025, written there with the index sets and for , that is, ; they classify it as an independent rediscovery, write that it was afterwards found independently by GPT-5.2 Pro with Aristotle, and cede priority. The same paper reports that the problem is essentially Problem 3 of Day 1 of the 2012 China Team Selection Test (Art of Problem Solving topic 469502, post 2628490), an occurrence recorded here as the paper reports it. Their report has its own page.
Depends on. No page of this wiki.
Acceptance. Thomas Bloom, the site's curator, marks the problem disproved, credits Somani on the problem page (last edited 12 January 2026) and records the formalization in the site's label; the community database records the problem as disproved with a Lean proof (last updated 10 January 2026). The result exists as the thread post and the Lean files, with no refereed write-up; the acceptance rests on the curator's documented review.