Papers With

← All papers
First page of Optimality of Wouter van Doorn's Upper Bound for the Mayer-Erdős Farey Problem

Optimality of Wouter van Doorn's Upper Bound for the Mayer-Erdős Farey Problem

Ricky Cipollini

math.NT Jul 25, 2026 · v1
formalization number-theory
Read PDF arXiv abstract Code
TL;DR
The proof was formalized in Lean 4 by Aristotle and van Doorn, with the formalization available in a public GitHub file.
Abstract
Let $\mathcal{F}_n$ be the Farey sequence of order $n$, written in increasing order. Call two fractions $\frac{a}{b} < \frac{c}{d}$ badly ordered if $a < c$ and $b > d$. Let $f(n)$ be the minimum number of Farey fractions strictly between two badly ordered fractions in $\mathcal{F}_n$. We prove $f(n)=\left(\frac{1}{4}+o(1)\right)n$. In the equivalent indexing convention of Erdős Problem 1005, this determines the requested asymptotic constant as $c=1/4$. The upper bound $f(n)\le n/4+O(1)$ was first obtained by Wouter van Doorn; the main result here is the matching lower bound.
Problem

Let f(n) be the minimum number of Farey fractions of order n lying strictly between two badly ordered fractions a/b < c/d, where a<c and b>d. Erdős Problem 1005 asks for the asymptotic constant c in f(n) cn. Van Doorn proved the upper bound f(n) ≤ n/4+O(1) and conjectured that it is optimal.

Approach

Every badly ordered pair is reduced to an elementary interval (a/b, (a+1)/(b-1)). The paper then shows that each such interval contains at least n/4 − o(n) Farey fractions, uniformly in a and b. The argument uses primitive progression counts, uniform Farey counts, Farey gap properties and an increment estimate for a weighted totient sum. The proof was formalized in Lean 4 by Aristotle and van Doorn.

Results

The paper proves f(n) = (1/4+o(1))n, so the asymptotic constant in Erdős Problem 1005 is c=1/4 and van Doorn's upper bound is optimal. The Lean formalization is publicly available.