Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 175
claims/: The 3 claim pages of Problem 175, one per claimant's result; the problem's standing derives from them.
Statement. Show that, for any , the binomial coefficient is not squarefree.
Status. PROVED (LEAN). The site labels the problem PROVED (LEAN) (page last edited 8 February 2026) and credits Sárközy for all sufficiently large and, independently, Granville and Ramaré and Velammal for every ; the three results are recorded on the claim pages Sárközy 1985 (partial), Velammal 1995 and Granville and Ramaré 1996. The Lean qualifier refers to Boris Alexeev's formalization of the Granville–Ramaré argument in his repository of formalized Erdős problems, which this corpus has not built; the two full proofs are refereed. The standing in the frontmatter derives from the claim pages.
Source. erdosproblems.com/175, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #175, https://www.erdosproblems.com/175.
References.
- [ErKo99] Erdős, Paul and Kolesnik, Grigori, Prime power divisors of binomial coefficients. Discrete Math. (1999), 101-117.
- [GrRa96] Granville, Andrew and Ramaré, Olivier, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients. Mathematika 43 (1996), no. 1, 73-107. Library home: granville_1996_explicit_bounds_exponential_sums_scarcity_squarefree.
- [Gu04] Guy, Richard K., Unsolved problems in number theory. Third edition, Problem Books in Mathematics, Springer, New York (2004), xviii+437 pp.; doi:10.1007/978-0-387-26677-0. Section B33 "Largest divisor of a binomial coefficient", printed p. 135, where the book states the conjecture and reports the Sárközy, Sander and Granville and Ramaré results. Library home: guy_2004_unsolved_problems_number_theory.
- [Sa85] Sárközy, A., On divisors of binomial coefficients, I. Journal of Number Theory 20 (1985), no. 1, 70-80.
- [Sa92] Sander, J. W., Prime power divisors of binomial coefficients. J. Reine Angew. Math. 430 (1992), 1-20. Library home: sander_1992_prime_power_divisors_binomial_coefficients.
- [Sa92b] Sander, J. W., On prime divisors of binomial coefficients. Bull. London Math. Soc. (1992), 140-142.
- [Sa95] Sander, J. W., On the order of prime powers dividing . Acta Math. (1995), 85-118.
- [Ve95] Velammal, G., Is the binomial coefficient square free?. Hardy-Ramanujan J. 18 (1995), 23-45. Library home: velammal_1995_is_binomial_coefficient_squarefree.
Formalization. Statement in formal-conjectures, which points to a Lean proof in Boris Alexeev's repository of formalized Erdős problems; that proof declares itself a formalization of the Granville–Ramaré argument and is linked, at its pinned commit, from their claim page. This corpus has not built it.
Current assessment
The question, as the site states it (page last edited 8 February 2026): is divisible by the square of a prime for every ? The answer is yes; the only squarefree central binomial coefficients are at .
Reduction. Kummer's theorem gives -adic valuation equal to the number of carries when is added to itself in base two, that is, the number of ones in the binary expansion of , so unless is a power of two; only , , needs an argument, and for those the square must come from an odd prime.
Proofs. Sárközy [Sa85] proved the statement for all sufficiently large by estimating exponential sums over primes, with no explicit threshold (partial claim page). Velammal [Ve95] made the bounds explicit with Vaughan's identity and exponent pairs, proving it for and checking the smaller range directly (claim page). Granville and Ramaré [GrRa96], independently, proved explicit bounds for the same exponential sums, obtaining a prime with for and checking the powers of two below, and sharpened this to a prime for every (claim page). Sander [Sa92], Theorem 1, proves more for large arguments: for every fixed and every large enough, with close to is divisible by the th power of a prime that itself tends to infinity, which contains the large- case of the problem; the site records it under the related question on the largest prime power dividing , so it has no claim page here. Both full proofs are refereed and the site's curator credits them; the Lean development in Alexeev's repository, first committed on 17 August 2026 and named as the formal proof by the formal-conjectures statement file, formalizes the Granville–Ramaré argument with Codex and GPT-5.6 Sol named as its formal authors, and is not built here. The site's label and the community database, which lists the formal status Lean as of its last update, dated 24 August 2026, name no development.
Related questions the site records, not part of the standing. Let be the largest exponent with for some prime . Sander [Sa92] showed and [Sa95] gave , improved by Erdős and Kolesnik [ErKo99] to ; the upper bound and the lower bound for almost all follow from Kummer's theorem, and whether for every is open. Sander [Sa92b] showed that is not squarefree for large when . Granville and Ramaré note that their Theorem 1* is close to best possible, since the largest prime whose square divides is . The site records as the largest known for which has no odd squared prime factor, and Guy's section B33 [Gu04] reports Erdős's belief that there is no larger one; Granville and Ramaré [GrRa96] settle this question of Erdős: Theorem 1* gives a prime with for every , their factorizations cover , and they state that is the largest central binomial coefficient not divisible by the square of an odd prime.
Search scope, 2026-10-07: the site's problem page, its discussion thread, the community database and the formal-conjectures file; 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.
- granville_1996_explicit_bounds_exponential_sums_scarcity_squarefree
- granville_1996_explicit_bounds_exponential_sums_scarcity_squarefree / theorem_1
- granville_1996_explicit_bounds_exponential_sums_scarcity_squarefree / theorem_1_star
- granville_1996_explicit_bounds_exponential_sums_scarcity_squarefree / theorem_9
- sander_1992_prime_power_divisors_binomial_coefficients
- sander_1992_prime_power_divisors_binomial_coefficients / theorem_1
- sander_1992_prime_power_divisors_binomial_coefficients / theorem_3
- velammal_1995_is_binomial_coefficient_squarefree
- velammal_1995_is_binomial_coefficient_squarefree / main_theorem
- velammal_1995_is_binomial_coefficient_squarefree / theorem_2
- velammal_1995_is_binomial_coefficient_squarefree / theorem_p24
- guy_2004_unsolved_problems_number_theory