Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 698

../

claims/: The 1 claim page of Problem 698, one per claimant's result; the problem's standing derives from them.


Statement. Is there some h(n)→∞h(n)\to \infty such that for all $2\leq i<j\leq n/2$

gcd((ni),(nj))≥h(n)?\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \geq h(n)?

Status. The site labels the problem PROVED (LEAN). The standing derived from the claim page is solved, proved, by Bergman 2011, whose bound tends to infinity with nn uniformly in ii (the claim page derives the explicit h(n)=n1/2/6h(n)=n^{1/2}/6 from it); a refereed paper credited by the site's curator. The Lean proofs the site's label refers to are third-party work not built here.

Source. erdosproblems.com/698, accessed 2026-09-04. The site attributes the problem to Erdős and Szekeres [ErSz78]. Cite as: T. F. Bloom, Erdős Problem #698, https://www.erdosproblems.com/698.

References.

Formalization. The formal-conjectures file FormalConjectures/ErdosProblems/698.lean, linked at its commit of 2026-09-19, states the question as erdos_698 with sorry, tags it solved and names as its formal proof, at a pinned commit, the file Erdos698.lean of Boris Alexeev's repository of Lean proofs, a copy of Wouter van Doorn's formalization with Aristotle; it also states the Erdős--Szekeres bound, its sharpness and Bergman's bound as variants, each with sorry, and names another copy of that file, the one Alexeev's repository keeps for an earlier Lean version, at its unpinned main revision, as the formal proof of the Bergman variant. The claim page links both Lean files at pinned commits. Nothing has been built here.

Current assessment

The question, as the site states it: is there a function h(n)→∞h(n)\to\infty with gcd⁡((ni),(nj))≥h(n)\gcd(\binom ni,\binom nj)\geq h(n) for all 2≤i<j≤n/22\leq i<j\leq n/2? The answer is yes.

What Erdős and Szekeres knew. Their identity (nj)(ji)=(ni)(n−ij−i)\binom nj\binom ji=\binom ni\binom{n-i}{j-i} shows that (ni)\binom ni divides (nj)(ji)\binom nj\binom ji, so the gcd is at least (ni)/(ji)≥2i\binom ni/\binom ji\geq 2^i and in particular exceeds 11; the bound grows with ii but not with nn, and is attained at i=1i=1, j=pj=p, n=2pn=2p for a prime pp, which is why the question asks for growth in nn.

The resolution. Bergman [Be11], Theorem 2, proves gcd⁡((ni),(nj))≥n1/22i−7/2/(i(i−1)1/2)\gcd(\binom ni,\binom nj)\geq n^{1/2}2^{i-7/2}/(i(i-1)^{1/2}) for 2≤i≤j≤n/22\leq i\leq j\leq n/2 and notes that the bound weakens to one independent of ii that tends to infinity with nn; the claim page's own minimization of the factor depending on ii, at least 1/61/6, gives h(n)=n1/2/6h(n)=n^{1/2}/6. In the site's thread, van Doorn (2026-01-16) rewrote the proof with the sharper constant 2in/(4ii−1)2^i\sqrt n/(4i\sqrt{i-1}) and formalized it in Lean with Aristotle; a copy of that file in Alexeev's repository is the formal proof the formal-conjectures record names. The claim page records the theorem, the sharper constant and the acceptance: a refereed paper credited by the site's curator; the Lean files are linked there and have not been built here. Bergman's paper bounds the size of the gcd and not its largest prime factor, which is the subject of Problem 699.

Search scope. As of 2026-10-07 the site's discussion thread holds one post, of 2026-01-16, and its proof-claims page lists no claim for the problem. The formal-conjectures statement file is described above at its commit of 2026-09-19 and the two Lean files at the commits the claim page links; none has been built here.

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.