`FormalConjectures/ErdosProblems/175.lean`

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 175

References:

erdosproblems.com/175
[Sa85] A. Sárközy, On divisors of binomial coefficients, I, J. Number Theory 20 (1985), 70–80.
[GrRa96] A. Granville and O. Ramaré, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients, Mathematika 43 (1996), 73–107.
[Ve95] G. Velammal, Is the binomial coefficient $\binom{2n}{n}$ square free?, Hardy-Ramanujan Journal 18 (1995), 23–45.

Sárközy proved the assertion for all sufficiently large n; Granville--Ramaré and Velammal independently proved the full range n ≥ 5.

Imports (1)

FormalConjecturesUtil

theorem Erdos175.erdos_175 sorry line 45 source
depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, Squarefree, Nat.choose, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.