Wiki
Wiki

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

∏i(2mimi)=∏j(2njnj)\prod_i \binom{2m_i}{m_i}=\prod_j \binom{2n_j}{n_j}

has infinitely many solutions in which all the indices mi,njm_i,n_j 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 a≥2a\ge2, with c=8a2+8a+1c=8a^2+8a+1,

(2aa)(4a+42a+2)(2cc)=(2a+2a+1)(4a2a)(2c+2c+1).\binom{2a}{a}\binom{4a+4}{2a+2}\binom{2c}{c} =\binom{2a+2}{a+1}\binom{4a}{2a}\binom{2c+2}{c+1}.

The verification is two lines. Write C(n)=(2nn)C(n)=\binom{2n}{n}, so that C(n+1)/C(n)=2(2n+1)/(n+1)C(n+1)/C(n)=2(2n+1)/(n+1). Then

C(a)C(a+1)=a+12(2a+1),C(2a+2)C(2a)=2(4a+1)(4a+3)(2a+1)(a+1),C(c)C(c+1)=c+12(2c+1),\frac{C(a)}{C(a+1)}=\frac{a+1}{2(2a+1)},\qquad \frac{C(2a+2)}{C(2a)}=\frac{2(4a+1)(4a+3)}{(2a+1)(a+1)},\qquad \frac{C(c)}{C(c+1)}=\frac{c+1}{2(2c+1)},

and the product of the three ratios is (4a+1)(4a+3)(c+1)/(2(2a+1)2(2c+1))(4a+1)(4a+3)(c+1)/\bigl(2(2a+1)^2(2c+1)\bigr), which equals 11 because c+1=2(2a+1)2c+1=2(2a+1)^2 and 2c+1=(4a+1)(4a+3)2c+1=(4a+1)(4a+3). For a≥2a\ge2 the six indices satisfy a<a+1<2a<2a+2<c<c+1a<a+1<2a<2a+2<c<c+1, so they are distinct, and different values of aa 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 b=0b=0 of the first is the family above. Kesarwani then counted 8,7778{,}777 solutions with every index at most 4040 (12 January 2026), most of them with a different number of indices on each side, the smallest such primitive solution having indices 5,7,195,7,19 against 1,2,3,6,201,2,3,6,20. Terence Tao gave an entropy argument (12 January 2026): products of central binomial coefficients over subsets of {1,…,N}\{1,\dots,N\} carry fewer than NN bits of information once NN is large, so two subsets must share a product. Nat Sothanaphan posted a counting version of Tao's argument and an exponential lower bound, (2/e)(1−o(1))N(2/\sqrt e)^{(1-o(1))N}, for the number of collisions with indices at most NN (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 a≥2a\ge2, 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 {k,2k−2,8k2−8k+2}\{k,2k-2,8k^2-8k+2\} and {k−1,2k,8k2−8k+1}\{k-1,2k,8k^2-8k+1\} for k≥3k\ge3, that is, a=k−1a=k-1; 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.