Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 397
claims/: The 2 claim pages of Problem 397, one per claimant's result; the problem's standing derives from them.
Statement. Are there only finitely many solutions to
with the distinct?
Status. DISPROVED (LEAN). The site labels the problem DISPROVED (LEAN) (page last edited 12 January 2026) and credits Neel Somani, working with ChatGPT, with an explicit infinite family of solutions, recorded on its claim page; the Lean qualifier refers to an Aristotle-generated formalization of that family, which this corpus has not built. The preprint of Feng and coauthors (29 January 2026) reports the same family, found by their Gemini-based agent Aletheia in December 2025, as a pending claim on its own page. There is no refereed write-up. The standing in the frontmatter derives from the claim pages.
Source. erdosproblems.com/397, accessed 2026-10-07. The site cites the problem from p. 77 of Erdős and Graham's 1980 problem book. Cite as: T. F. Bloom, Erdős Problem #397, https://www.erdosproblems.com/397.
References.
- [ErGr80] Erdős, P. and Graham, R. L., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique 28, Université de Genève (1980), p. 77. Library home: erdos_1980_old_new_problems_results_combinatorial_number_theory.
Formalization. Statement in
formal-conjectures,
pinned to the commit of 18 September 2026. At that commit the file states erdos_397 : answer(False) ↔ …Finite with
sorry, credits the negative answer to Somani in its docstring, and names as
its formal proofs an Aristotle-generated gist and a proof in a fork of the
repository; both are linked, at pinned revisions, from
the claim page,
together with the copy of the gist in Boris Alexeev's repository of Lean
proofs. This corpus has built none of the three.
Current assessment
The question, as the site states it (page last edited 12 January 2026): can two products of central binomial coefficients , taken over two index sets with no index in common, be equal in more than finitely many ways? They can, so the finiteness asked for fails.
The resolution. Somani's family (thread post of 11 January 2026, proof by ChatGPT): for and , the indices and give equal products. The identity reduces, through the ratio , to the two factorizations and , and the six indices are distinct for . The claim page records the verification, the Lean files at their pinned revisions and the acceptance: the site's curator credits Somani and the community database records the problem as disproved with a Lean proof (last updated 10 January 2026); there is no refereed write-up, and no Lean file is built here.
Further constructions in the thread. Sharvil Kesarwani gave two two-parameter families, found by a computer search for one-parameter families (11 January 2026; one case of the first is Somani's family), and an exhaustive count of solutions with all indices at most (12 January 2026), most of them with a different number of indices on each side, the smallest such primitive solution having three indices on one side and five on the other. Terence Tao gave an entropy argument that forces coincidences among the products over subsets of for large (12 January 2026). Nat Sothanaphan posted a counting version of Tao's argument and an exponential lower bound, , for the number of coincidences with indices at most (13 and 14 January 2026); both came from ChatGPT, as his posts state, and he wrote that he had not fully checked the counting rewrite. These posts confirm the answer by other routes and have no claim page, since the site credits the disproof to Somani and they are not dated manuscripts. 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; whether that construction gives infinitely many solutions with distinct indices was discussed in the thread and not settled, so it is context here and not a claim.
An earlier occurrence and an independent report. Feng and twenty-three coauthors (arXiv:2601.22401, first posted 29 January 2026; the card is linked below) report in Section 4.1 of their case study that their Gemini-based research agent Aletheia, run from 2 to 9 December 2025, produced the same family: their Theorem 4 takes the index sets and for , which is Somani's family with . They classify the result as an independent rediscovery, write that the family was afterwards found independently by GPT-5.2 Pro with Aristotle, and cede priority. Their Remark 4.1 and introduction also report that the problem is essentially Problem 3 of Day 1 of the 2012 China Team Selection Test, posted on Art of Problem Solving as topic 469502, post 2628490; that occurrence is recorded here as the paper reports it. The report is a pending claim on its own page; the site credits the disproof to Somani alone.
Search scope: the site's problem page, its discussion thread, the community database, the formal-conjectures statement file and the two Lean proofs it names, the copy of the gist in Alexeev's repository, and the library's card of the Feng et al. preprint (arXiv:2601.22401v3); the site lists no proof claim for the problem.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.