248.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/248
[TaTe25] T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers. arXiv:2512.01739 (2025).

Imports (1)

theorem Erdos248.erdos_248 sorry line 40 source
depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Set.Infinite, Nat, Set.ofPred, GE.ge, LE.le, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, HAdd.hAdd, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.