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 698 is yes. Bergman proves (Theorem 2 of the paper and its equations (7) and (8); the library card is Bergman 2011) that for
Bergman notes that (8) weakens to a bound tending to infinity with that is independent of , which answers the question; the explicit constant is this page's own elementary consequence of (8), not a statement of the paper: the factor is at least , its value at , for every , so whenever , and works. The proof lets the symmetric group act on pairs of two-block decompositions of with block sizes and ; the orbit sizes are all divisible by the least common multiple of the two coefficients, the combination is divisible by and small after its leading terms cancel, and the resulting bound on becomes a bound on the gcd through . The question comes from Erdős and Szekeres (Erdős and Szekeres 1978), whose identity gives , a bound that grows with but not with and is attained for , and with prime; they asked for growth in uniform over , which Bergman's bound supplies.
A sharper constant. In the site's discussion thread on 2026-01-16, Wouter van Doorn posted a rewritten proof along Bergman's lines giving for , which improves Bergman's constant, together with the Lean formalization below. The post is a thread comment on Bergman's result, so it is disclosed here and has no page of its own.
Formalization. The Lean file ErdosProblem698.lean in van Doorn's
repository names Bergman as the author of the original proof, van Doorn as the
author of the rewritten proof and the AI system Aristotle (Harmonic) as the
formalizer; its theorem binomial_gcd_lower_bound states van Doorn's
inequality, which implies the problem's statement with . The
thread post of 2026-01-16 links the file, which the repository's history dates
to 2026-03-02; the link above pins that commit. A copy in Boris Alexeev's
repository of Lean proofs, Erdos698.lean, declares itself a formalization of
a solution to the problem with Bergman as its informal author and Aristotle
and van Doorn as its formal authors; its theorem erdos_698 states the same
inequality, and the formal-conjectures statement file, at the commit of
2026-09-19 the problem page links, tags erdos_698 solved and names that copy
at the linked commit as its formal proof. Neither file contains sorry at its
linked commit. Both files declare themselves formalizations of Bergman's
result, so they are links on this page; this corpus has not built or audited
either, so the page lists no formalized evidence.
Depends on. No page of this wiki.
Acceptance. The site's curator, T. F. Bloom, marks the problem proved and
credits this paper, which the page lists as reviewed. The paper is G. M.
Bergman, On common divisors of multinomial coefficients, Bull. Aust. Math.
Soc. 83 (2011), no. 1, 138--157, published online 2010-10-13, a refereed
journal, listed as refereed. The page is dated by the first version of the
arXiv preprint, posted 2008-06-03; the second version of 2010-03-20 is the one
the journal printed.