FormalConjectures/ErdosProblems/1005.lean

GitHub source file

5 declarations, 2 contain sorry, 0 declared as axioms

1. def Erdos1005.IsFarey A rational q is a Farey fraction of order n if it lies in [0, 1] and has denominator at most n line 43 source

   Source documentation

   A rational q is a Farey fraction of order n if it lies in [0, 1] and has denominator at most n. (Every q : ℚ is stored in lowest terms, so q.den and q.num are the reduced denominator and numerator.)

   standard axioms: Quot.sound, propext what this means

   Statement uses: Nat, Rat

   Proof uses: And, LE.le, OfNat.ofNat, Rat.den

   3 instances, coercions and auxiliary constants left out.

   def IsFarey (n : ℕ) (q : ℚ) : Prop :=
   …

2. def Erdos1005.betweenCount The number of Farey fractions of order n strictly between x and y line 47 source

   Source documentation

   The number of Farey fractions of order n strictly between x and y.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat, Rat

   Proof uses: Set.ncard, Set.ofPred, And, Erdos1005.IsFarey, LT.lt

   1 instances, coercions and auxiliary constants left out.

   noncomputable def betweenCount (n : ℕ) (x y : ℚ) : ℕ :=
   …

3. def Erdos1005.f Documented declaration: f line 54 source

   Source documentation

   f n is the largest integer such that any two Farey fractions of order n whose indices differ by at most f n are similarly ordered: it is the minimum, over all pairs x < y of Farey fractions of order n with (x.num - y.num) * (x.den - y.den) < 0, of the number of Farey fractions strictly between x and y.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat

   Proof uses: InfSet.sInf, Set.ofPred, Exists, Rat, And, Erdos1005.IsFarey, LT.lt, Int, HMul.hMul, HSub.hSub, Rat.num, Rat.den, OfNat.ofNat, Eq, Erdos1005.betweenCount

   10 instances, coercions and auxiliary constants left out.

   noncomputable def f (n : ℕ) : ℕ :=
   …

4. theorem Erdos1005.erdos_1005 Let $\frac{a_1}{b_1}, \frac{a_2}{b_2}, \ldots$ be the Farey fractions of order $n \geq 4$ sorry line 70 source

   Source documentation

   Let $\frac{a_1}{b_1}, \frac{a_2}{b_2}, \ldots$ be the Farey fractions of order $n \geq 4$. Let $f(n)$ be the largest integer such that if $1 \leq k < l \leq k + f(n)$ then $\frac{a_k}{b_k}$ and $\frac{a_l}{b_l}$ are similarly ordered, in other words $(a_k - a_l)(b_k - b_l) \geq 0$. Estimate $f(n)$: in particular, is there a constant $c > 0$ such that $f(n) = (c + o(1)) n$ for all large $n$?

   Mayer [Ma42] proved that $f(n) \to \infty$ and Erdős [Er43] that $f(n) \gg n$. Van Doorn [vD25b] proved $(1/12 - o(1)) n \le f(n) \le n / 4 + O(1)$ and conjectured that $f(n) = (1/4 + o(1)) n$, which was proved by Cipollini and GPT-5.5; see erdos_1005.variants.constant.

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Real, And, LT.lt, OfNat.ofNat, Filter.Tendsto, Nat, HDiv.hDiv, Erdos1005.f, Filter.atTop, nhds

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   25 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1005 : answer(True) ↔
       ∃ c : ℝ, 0 < c ∧ Tendsto (fun n : ℕ => (f n : ℝ) / n) atTop (𝓝 c) := by
   …

   Mentions: c, Erdos1005.f

5. theorem Erdos1005.erdos_1005.variants.constant sorry line 78 source

   depends on sorry what this means

   Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, Erdos1005.f, Filter.atTop, nhds, OfNat.ofNat

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.