Combinatorics

Motivation

Minimizing the sum of weighted completion times $\sum_j w_jC_j$ is one of the standard objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. With release dates or precedence constraints the problem is NP-hard already on one machine, and on $m$ identical parallel machines it is harder still, so the literature of the 1990s concentrated on approximation algorithms. Many of these, including LP-based ones, are naturally designed for a single machine, where an order of the jobs determines the schedule.

Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) gave a generic way to move from one machine to many. Their §4 describes an algorithm, Delay List, that takes any one-machine schedule as a priority list and produces an $m$-machine schedule, and proves that a $\rho$-approximate one-machine schedule yields a $\bigl((1+\beta)\rho+1+1/\beta\bigr)$-approximate $m$-machine schedule for every $\beta>0$. The guarantee holds with release dates and arbitrary precedence constraints simultaneously, which at the time gave the best bounds known for several special cases, for example a factor 4 for series-parallel precedence without release dates.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has processing time $p_j>0$, release date $r_j\ge 0$ and weight $w_j>0$. Precedence constraints form a strict partial order $\prec$: $i\prec j$ means that $J_j$ may start only after $J_i$ completes.

A feasible nonpreemptive schedule on $m$ machines assigns each job a start time $S_j$ and a machine; each job runs uninterrupted for $p_j$ time units on its machine, two jobs on one machine do not overlap, $S_j\ge r_j$, and $S_i+p_i\le S_j$ whenever $i\prec j$. The completion time is $C_j=S_j+p_j$ and the value of the schedule is $\sum_j w_jC_j$. A one-machine schedule is the case $m=1$.

The critical-path length $\kappa_j$ (Definition 4.1) is $p_j+r_j$ for a job without predecessors and $p_j+\max\{\max_{i\prec j}\kappa_i,\,r_j\}$ otherwise; it is the earliest time $J_j$ could complete with unlimited machines.

A list is an ordering $\pi$ of the jobs. Delay List with parameter $\beta>0$ processes time continuously. A job is ready once it is released and all its predecessors have completed; $q^m_j$ is the time it becomes ready. The head is the first unscheduled job of the list. Idle machine-time is recorded as charged to jobs. Whenever a machine is idle:

1. if the head is ready, it is started, and charged all uncharged idle time in $(q^m_j,s^m_j)$;
2. otherwise the first ready job $J_k$ of the list is started as soon as at least $\beta p_k$ units of uncharged idle time have accumulated, and is charged $\beta p_k$ of it;
3. otherwise nothing happens.

For a job $J_i$, $B_i$ is the set of jobs up to and including $J_i$ in the list, $A_i$ the set after it, $O_i\subseteq A_i$ the set of jobs of $A_i$ started before $J_i$, and $p(A)=\sum_{k\in A}p_k$. Definition 4.4 builds from the schedule a backward path $P'_i$ ending at $J_i$, whose length is $\kappa'_i$.

Formalization targets

Goal: Theorem 4.13

Let $S^1$ be a feasible one-machine schedule of the instance with $\sum_j w_jC^1_j\le\rho\sum_j w_jC'_j$ for every feasible one-machine schedule $C'$. Let $m\ge 2$ and $\beta>0$. Every Delay List schedule $S^m$ built on the completion order of $S^1$ satisfies, for every feasible $m$-machine schedule $N$,

$$\sum_j w_jC^m_j\le\Bigl((1+\beta)\rho+1+\frac1\beta\Bigr)\sum_j w_jC^N_j .$$

Milestones, in the order the proof uses them

• Fact 4.5: $\kappa'_i\le\kappa_i$.
• Fact 4.6: the idle time charged to $J_i$ is at most $\beta p_i$.
• Lemma 4.7: no uncharged idle time remains in $(q^m_i,s^m_i)$, and that idle time is charged only to jobs in $B_i$.
• Lemma 4.8: the idle time charged to $A_i$ within $(0,s^m_i)$ is at most $m(\kappa'_i-p_i)$, so $p(O_i)\le m(\kappa'_i-p_i)/\beta\le m(\kappa_i-p_i)/\beta$.
• Theorem 4.9: $C^m_i\le(1+\beta)p(B_i)/m+(1+1/\beta)\kappa'_i-p_i/\beta$ for any list obeying precedence.
• Lemma 4.10: $C^m_{\mathrm{OPT}}\ge C^1_{\mathrm{OPT}}/m$.
• Lemma 4.11: $C^m_{\mathrm{OPT}}\ge\sum_i w_i\kappa_i=C^\infty_{\mathrm{OPT}}$.
• Corollary 4.12: $C^m_i\le(1+\beta)C^1_i/m+(1+1/\beta)\kappa_i$ when the list is the completion order of $S^1$.

A further item states that a Delay List schedule exists for every instance and every list, so that the goal does not hold vacuously.

Significance

The result. Theorem 4.13 turns every one-machine approximation algorithm for weighted completion time with release dates and precedence into an $m$-machine algorithm at a bounded loss. With an optimal one-machine schedule and $\beta=1$ the factor is $4$ (Corollary 4.14, for series-parallel orders), and the bounds are job-by-job (Theorem 4.9, Corollary 4.12), which the paper uses in Remark 4.15 to extend the method to other metrics and to one-machine schedules that ignore release dates. The same algorithm is the engine of the paper's $2\sqrt2$-approximation for parallel machines with release dates (§4.5).

Formalizing it. The theorem has been proved since 1997 (SODA) and 2001 (journal). There is no machine-checked version of it or of any of its lemmas, and the platform currently has no model of scheduling with release dates and precedence constraints. A formalization produces a precise specification of Delay List, whose informal description is given in discrete time and repaired in a remark; a checked proof of the charging argument; and reusable lower bounds (Lemmas 4.10 and 4.11) for any later work on parallel-machine scheduling with precedence.

Difficulty

The obvious attempt, list scheduling (start the first available job of the list whenever a machine is free), fails with non-identical processing times: a long job taken out of order can occupy a machine and delay a more valuable job that becomes ready shortly afterwards. Delay List allows out-of-order jobs only against accumulated idle time, and the analysis rests on a charging invariant. Stating it needs care about time (the paper's discrete-time exposition can over-charge by a time unit), about which idle time a charge consumes, and about many jobs being scheduled at one instant. The bound must hold simultaneously for release dates and arbitrary precedence constraints, where idle machines can be forced both by jobs that are not yet released and by chains of predecessors, and it must hold for every tie-breaking choice of the algorithm.

Formalization scope

Jobs are Fin n, machines Fin m, and times are real numbers. Processing times are positive, release dates nonnegative and weights positive, as in §1. Precedence is a strict partial order, the transitive closure of the paper's DAG; $\kappa$, readiness and feasibility are unchanged by taking the closure. The optimum is never a real infimum: "within a factor $\rho$ of an optimal one-machine schedule" and "within a factor $c$ of an optimal $m$-machine schedule" are inequalities against every feasible schedule of the same instance, with the same release dates and precedence constraints.

Delay List is formalized in the continuous-time version described in the proof of Fact 4.6, as a predicate on runs that records start times, machines, the order in which jobs are scheduled at equal times, and charge windows. A case-2 charge takes the most recent uncharged idle time, and idle time is charged by whole time slices. Every guarantee is claimed for every run satisfying the predicate. The ties in Definition 4.4 are broken arbitrarily, so statements involving $\kappa'_i$ hold for every admissible path. Lemma 4.10 uses nonpreemptive one-machine schedules. Lemma 4.11's $C^\infty_{\mathrm{OPT}}$ is modelled by $n$ machines.

It would be trivializing to assume the conclusions of Fact 4.6 or Lemma 4.7 as properties of the run, or to measure $\rho$ against a relaxation without release dates or precedence; both are ruled out. The algorithm's rules are the only hypotheses on the run.

Not stated: the running time of Delay List; the discrete-time algorithm; Corollary 4.14 (it needs a formal class of series-parallel orders and the external one-machine algorithm of Adolphson for them); Remark 4.15 (release-date-free one-machine schedules), whose hypotheses the paper does not pin down; and the extension to delays between jobs. Contributions of general infrastructure, such as idle-time accounting for step functions and lemmas about list schedules under precedence, are welcome and reusable beyond this mission.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM Journal on Computing 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• R. L. Graham, Bounds for certain multiprocessing anomalies, Bell System Technical Journal 45:1563–1581, 1966. https://doi.org/10.1002/j.1538-7305.1966.tb01709.x
• D. Adolphson, Single machine job sequencing with precedence constraints, SIAM Journal on Computing 6(1):40–54, 1977. https://doi.org/10.1137/0206002

Motivation

Minimizing the average completion time of jobs that arrive over time is a basic objective in machine scheduling. It measures how long a job spends in the system on average. With several identical machines, release dates and no preemption (written $P|r_j|\sum C_j$), the problem is strongly NP-hard already on one machine. Research has therefore looked for approximation algorithms: polynomial-time rules whose total completion time is provably within a constant factor of every feasible schedule.

A common approach solves a relaxation that is easy to optimize and converts its solution into a feasible schedule. Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) use a relaxation that needs neither linear programming nor dynamic programming: pretend that the $m$ machines are one machine that is $m$ times as fast, and allow preemption.

Timeline:

• 1996, Chakrabarti, Phillips, Schulz, Shmoys, Stein and Wein (ICALP 1996, LNCS 1099, pp. 646–657): a $(2.89+\epsilon)$-approximation for $P|r_j|\sum C_j$.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), §3 and §4.5). §3 gives a simple $(3-1/m)$-approximation by list scheduling from the one-machine relaxation. §4.5 combines it with the Delay List conversion to obtain $2\sqrt2\approx2.83$. This mission's goal is the §4.5 result.
• 1999, Afrati, Bampis, Chekuri, Karger, Kenyon, Khanna, Milis, Queyranne, Skutella, Stein and Sviridenko (FOCS 1999, pp. 32–43): polynomial-time approximation schemes for $P|r_j|\sum w_jC_j$. These settle the approximability, but the algorithms are far more involved than the ones formalized here.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$ and $m\ge1$ identical machines. Job $J_j$ has a processing time $p_j>0$ and a release date $r_j\ge0$.

A feasible schedule gives each job a start time $S_j\ge r_j$ and a machine. Job $J_j$ runs without interruption on its machine during $[S_j,S_j+p_j)$, and two jobs on the same machine never overlap. The completion times are $C_j=S_j+p_j$ and the objective is $\sum_j C_j$. $C^*_j$ denotes the completion times of an arbitrary feasible schedule, against which every bound is stated.

The one-machine relaxation $I1$ has the same jobs and a single machine. Job $J_j$ has processing time $p_j/m$ and release date $r_j$ in $I1$, and may be preempted. A preemptive schedule $P1$ of $I1$ gives each job a processing rate $\rho_j(t)\ge0$. The rates sum to at most $1$ at each time, and no job is processed before its release date. Each job receives $p_j/m$ units in total. Its completion time $C^{P1}_j$ is the first time by which all of it has been processed. $P1$ is optimal if $\sum_j C^{P1}_j$ is minimal among all such schedules.

A list is an ordering $\pi$ of the jobs, and the completion order of $P1$ lists the jobs by nondecreasing $C^{P1}_j$. Two ways of turning a list into an $m$-machine schedule are compared.

• Strict-order list scheduling gives the schedule $N$. The jobs start in the order of the list. Each job starts at the earliest time that is no earlier than its release date, no earlier than the previous job's start, and at which some machine is free.
• Delay List with parameter $\beta>0$ gives the schedule $D$. When a machine is idle, Delay List starts the first unscheduled job of the list if it has been released. If that job has not been released, the first released job of the list may jump ahead, but only once at least $\beta p_j$ units of idle time (machine × time) have accumulated that no earlier job has charged. The job then charges exactly that amount. A job started in list order charges all uncharged idle time since its release.

Formalization targets

Goal: Lemma 4.19

With $P1$ optimal, $\pi$ its completion order, $N$ the strict-order list schedule of $\pi$ and $D$ a Delay List schedule of $\pi$ with $\beta_0=\sqrt{3-2\sqrt2}$, every feasible schedule satisfies

$$\min\Bigl(\sum_j C^N_j,\ \sum_j C^D_j\Bigr)\le 2\sqrt2\,\sum_j C^*_j .$$

The printed lemma says $2.83$. Its proof gives $2\sqrt2\approx2.8284$, which is stated here.

Milestones

In the order the proof uses them:

1. (4.2): if $\sum_j p_j>\alpha\sum_j C^*_j$ then $\sum_j r_j\le(1-\alpha)\sum_j C^*_j$.
2. Lemma 3.1: $\sum_j C^{P1}_j\le\sum_j C^*_j$ for $P1$ optimal.
3. (3.3): $\sum_j C^N_j\le 2\sum_j C^{P1}_j+(1-1/m)\sum_j p_j$ for any $P1$.
4. Lemma 3.2: $\sum_j C^N_j\le(3-1/m)\sum_j C^*_j$.
5. Theorem 4.9, specialised to no precedence constraints. With $B_i$ the jobs at or before $J_i$ in the list,

$$C^D_i\le\frac{(1+\beta)p(B_i)}{m}+\Bigl(1+\frac1\beta\Bigr)(r_i+p_i)-\frac{p_i}{\beta}.$$

6. Lemma 4.18: $\sum_j C^D_j\le(2+\beta)\sum_j C^*_j+\frac1\beta\sum_j r_j$.
7. The balanced bound: under (4.2)'s hypothesis, $\sum_j C^D_j\le(2+\beta+(1-\alpha)/\beta)\sum_j C^*_j$.
8. The constants: at $\alpha=2\sqrt2-2$ and $\beta=\sqrt{3-2\sqrt2}$, $2+\alpha=2+\beta+(1-\alpha)/\beta=2\sqrt2$.

Two existence statements accompany them. One says an optimal $P1$ exists. The other says a Delay List schedule exists for every list and every $\beta>0$.

Significance

The result gives a $2\sqrt2$-approximation for $P|r_j|\sum C_j$ that is simple to state and runs in $O(n\log n)$ time. It improves the $2.89+\epsilon$ bound of Chakrabarti et al. Neither of its two algorithms achieves the ratio alone. It comes from an analysis in which each algorithm is good exactly when the other is bad. List scheduling is good when processing times are small relative to the optimum. Delay List is good when release dates are small. The inequality (4.2) connects the two cases.

The component results are reusable beyond this paper. The one-machine relaxation lower bound (Lemma 3.1) and the $(3-1/m)$ bound for list scheduling from it (Lemma 3.2) apply to any conversion from a fast single machine. The per-job bound of Theorem 4.9 is the core of the Delay List technique. Its general form, with precedence constraints, drives the paper's results for precedence-constrained scheduling.

All results are proved in the paper. None of them has a machine-checked proof that this mission knows of. A formalization would check the Delay List charging argument, which the paper states only in discrete time and adapts to continuous time in one sentence. It would also produce reusable Lean definitions of parallel-machine schedules with release dates and of list scheduling.

Difficulty

The arithmetic of the goal is routine once the milestones are in place. The substance lies in two places.

The first is Lemma 3.1 together with the "standard makespan argument" behind (3.2). The one-machine relaxation must be related to the $m$-machine schedule, and to the list schedule, with care about release dates. In particular, in the list schedule every machine is busy between the last release among the first $j$ jobs of the list and the start of the $j$-th job. Proving this needs the strict order.

The second, and harder, is Theorem 4.9. The obvious argument bounds the waiting time of job $J_i$ by the work of the jobs ahead of it, but Delay List lets later jobs jump ahead. The idle time before $J_i$ starts and the work of the jobs that jump ahead of it must both be controlled, and the paper's charging argument for this depends on where charged idle time lies on the time axis and on which jobs charged it. Making that bookkeeping precise for a continuous-time algorithm is the main formalization cost.

Formalization scope

Jobs are Fin n and machines Fin m with $m\ge1$. Times are real, processing times are positive and release dates nonnegative. There are no weights and no precedence constraints. "Optimal" is never an infimum. Every bound is stated against every feasible nonpreemptive schedule, and $P1$'s optimality is the hypothesis that its total completion time is at most that of every preemptive schedule of $I1$.

Committed conventions:

• Preemptive schedules of $I1$ are rate functions, so the machine of $I1$ may be shared. The paper's one-job-at-a-time schedules are a special case.
• Lists are bijections Fin n ≃ Fin n. A list of $P1$ may break ties in completion time in any way, and every such list is covered.
• $N$ is the strict-order variant of list scheduling, which footnote 3 of the paper contrasts with the greedy variant used in §4. It is a recursive definition over list positions.
• Delay List is the continuous-time algorithm, as adopted in the proof of Fact 4.6. It is a predicate on start times, machines, the scheduling order and charge windows. A job scheduled out of order takes its charge from the most recent uncharged idle time; the paper leaves this placement open. Theorem 4.9 and Lemma 4.18 assume $m\ge2$, the setting of §4.1. The goal assumes only $m\ge1$.
• The printed Lemma 4.18 lacks a $\sum_j$ on the $C^*$ term. The summed form of its proof's last display is stated.

The statement cannot be made easy by the hypotheses. Two existence items show that an optimal $P1$ and a Delay List schedule always exist, so no statement is vacuous. The bound is against every feasible schedule, not against the relaxation's value.

Not stated: the $O(n\log n)$ running time, the on-line version of §3's algorithm, and Delay List with precedence constraints (Theorem 4.9 in general, which is the subject of mission III of this series). Contributions welcome: proofs of the milestones, and reusable lemmas on list scheduling with release dates.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• S. Chakrabarti, C. A. Phillips, A. S. Schulz, D. B. Shmoys, C. Stein, J. Wein, Improved scheduling algorithms for minsum criteria, in Proceedings of ICALP 1996, LNCS 1099, Springer, pp. 646–657 (reference [3] of the paper).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, in Proceedings of the 40th IEEE FOCS, 1999, pp. 32–43 (reference [2] of the paper).

Motivation

Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written $1|r_j|\sum C_j$), the problem is strongly NP-hard, so research has focused on approximation algorithms whose guarantees are stated against every feasible schedule.

The standard route runs through the preemptive relaxation. When jobs may be interrupted and resumed, the shortest-remaining-processing-time rule (SRPT) produces an optimal schedule, and its value is a lower bound for every nonpreemptive schedule. The question is how to turn that preemptive schedule into a nonpreemptive one without losing too much.

Timeline:

• 1995, Phillips, Stein and Wein (WADS 1995, pp. 86–97): order the jobs by their SRPT completion times and schedule them nonpreemptively in that order. This gives a 2-approximation. Later 2-approximations are by Hoogeveen and Vestjens (IPCO 1996), Stougie (1995), and Goemans (SODA 1997). Hoogeveen and Vestjens also showed that deterministic on-line algorithms cannot beat 2.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1)): order by $\alpha$-points instead of completion times, choose $\alpha$ at random, and take the best $\alpha$ off-line. This gives the $e/(e-1)\approx1.58$ bound for Best-$\alpha$ that is the goal of this mission, and an optimal randomized on-line algorithm.
• 1999, Afrati et al. (FOCS 1999): a polynomial-time approximation scheme for $1|r_j|\sum w_jC_j$. This settled the approximability of the problem, but the resulting algorithms are far from simple.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has a processing time $p_j>0$, a release date $r_j\ge0$, and, where the objective is weighted, a weight $w_j>0$. There is one machine.

A nonpreemptive schedule assigns each job a start time $S_j\ge r_j$ such that the intervals $[S_j,S_j+p_j)$ are pairwise disjoint. Its completion times are $C_j=S_j+p_j$.

A preemptive schedule $P$ specifies, for each time $t$, which job runs at $t$, if any. Job $J_j$ runs only at times $t\ge\max(0,r_j)$, receives exactly $p_j$ units of processing in total, and finishes by some finite time. Its completion time $C^P_j$ is the first time by which all of $J_j$ has been processed. For $\alpha\in(0,1]$, its $\alpha$-point $C^P_j(\alpha)$ is the first time by which $\alpha p_j$ units have been processed.

For a job $J_i$, $T_i$ denotes the idle time of $P$ before $C^P_i$. $x_{ij}$ denotes the fraction of $J_j$ processed before $C^P_i$. The paper writes $S^P_i(\beta)$ for the set of jobs with $x_{ij}=\beta$, and also for their total processing time.

One-machine list scheduling in a given order runs the jobs nonpreemptively in that order. Each job starts at the later of its release date and the completion of the previous job in the list. An $\alpha$-schedule is list scheduling in nondecreasing order of the $\alpha$-points $C^P_j(\alpha)$. $C^\alpha_j$ denotes the completion times of an $\alpha$-schedule.

Random-$\alpha$ draws $\alpha$ from a distribution on $(0,1]$ and outputs the $\alpha$-schedule. Best-$\alpha$ outputs the $\alpha$-schedule of smallest total completion time $\min_\alpha\sum_j C^\alpha_j$.

Formalization targets

Goal: Corollary 2.7

Let $P$ be optimal among preemptive schedules for $\sum_j C_j$. Then there is $\alpha\in(0,1]$ such that every $\alpha$-schedule derived from $P$ satisfies

$$\sum_j C^\alpha_j\;\le\;\frac{e}{e-1}\sum_j C_j\qquad\text{for every feasible nonpreemptive schedule } (C_j)_j .$$

Since Best-$\alpha$ returns a schedule no worse than this $\alpha$-schedule, Best-$\alpha$ is an $e/(e-1)$-approximation.

Milestones

1. The calculus behind the constant. For $f(\alpha)=e^\alpha/(e-1)$ and every $\beta\in(0,1]$,

$$\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha=\frac1{e-1}.$$

2. Lemma 2.2: $C^P_i=T_i+\sum_{0<\beta\le1}\beta S^P_i(\beta)$.
3. Lemma 2.3: $C^\alpha_i\le T_i+(1+\alpha)\sum_{\beta\ge\alpha}S^P_i(\beta)+\sum_{\beta<\alpha}\beta S^P_i(\beta)$.
4. Lemma 2.5: if $\alpha$ has density $f$ on $(0,1]$, then $E[C^\alpha_i]\le(1+\delta)C^P_i$ with $\delta=\max_{0<\beta\le1}\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha$.
5. Theorem 2.6, for the weighted objective with $P$ optimal among preemptive schedules: the expected approximation ratio of Random-$\alpha$ is at most $2$ for uniform $\alpha$, at most $1.8$ for $\alpha=1$ w.p. $3/5$ and $\alpha=1/2$ w.p. $2/5$, and at most $e/(e-1)$ for the density $e^\alpha/(e-1)$.

Companion statements, not milestones:

• the upper bound of Theorem 2.1, $\sum_jC^\alpha_j\le(1+1/\alpha)\sum_jC^P_j$;
• the existence of an optimal preemptive schedule.

Significance

The $e/(e-1)$ bound shows that conversion from the preemptive relaxation can beat the factor 2 of the natural ordering. It does so by exploiting that no single instance is bad for many values of $\alpha$ at once. The $\alpha$-point technique was also used with LP relaxations, for example by Goemans (SODA 1997) and by Schulz and Skutella. The randomized version is an optimal randomized on-line algorithm for $1|r_j|\sum C_j$. Lemma 2.3 is a statement about any preemptive schedule, so it applies wherever a good preemptive or fractional schedule is available.

All results of the mission are proved in the paper, except that the proof of Theorem 2.6, part 2 is omitted there. No machine-checked proof of them is known. A complete development would give a verified model of preemptive one-machine schedules, $\alpha$-points and list scheduling, together with the averaging argument over $\alpha$. These are reusable for the later results of the same paper and for the $\alpha$-point literature.

Difficulty

The obvious argument bounds each job's $\alpha$-schedule completion time directly against its preemptive completion time. That argument loses a factor $1+1/\alpha$ (Theorem 2.1), which is at least 2 for every fixed $\alpha$. The improvement needs Lemma 2.3. There the charge to each job depends on how much of it was done by $C^P_i$ relative to $\alpha$, and the idle time $T_i$ is not inflated at all. Proving Lemma 2.3 requires reasoning about a preemptive schedule as a measure on time, and about how moving pieces of jobs changes completion times. A proof that treats the preemptive schedule as a finite list of pieces must first show that nothing is lost by this discretization.

The averaging step needs the expectation over $\alpha$ to be an honest integral. The map $\alpha\mapsto C^\alpha_i$ must be shown integrable, which requires a fixed rule for ties between equal $\alpha$-points.

Formalization scope

• Model. Jobs are Fin n, time is real, $p_j>0$ and $r_j\ge0$. The paper admits $p_j=0$ only in its tightness instances.
  • A preemptive schedule is a function $\sigma:\mathbb R\to$ Option (Fin n) (none = idle). Each job's run set is measurable, lies in $[\max(0,r_j),\infty)$, is bounded above, and has Lebesgue measure $p_j$.
  • Completion times and $\alpha$-points are infima of nonempty sets that are bounded below.
  • $T_i$ is the measure of the idle set in $[0,C^P_i)$.
  • The paper's sums over $\beta$ are sums over jobs, weighted by the fraction $x_{ij}$.
• List scheduling is strict: jobs never overtake the list order, and the machine is free from time $0$.
  • Lemma 2.3, Theorem 2.1, Theorem 2.6.2 and the goal hold for every tie-break among equal $\alpha$-points.
  • The expectations (Lemma 2.5, Theorem 2.6.1 and 2.6.3) use the tie-break by job index. They assert integrability as part of the conclusion.
• Optimality. "Approximation ratio $c$" is stated as an inequality against every feasible nonpreemptive schedule, never against an infimum.
  • The optimality of $P$ among preemptive schedules is the paper's standing assumption for its upper bounds (p. 151). It appears as a hypothesis of Theorem 2.6 and of the goal.
  • The lemmas hold for arbitrary $P$ and do not carry it.
  • An existence statement shows the hypothesis can be met.
• Lemma 2.5's $\delta$ is replaced by any upper bound of the integrals over $\beta\in(0,1]$. This is equivalent, and it avoids assuming that the maximum is attained.
• Not stated:
  • the running time $O(n^2)$ of Best-$\alpha$ and the optimality of SRPT;
  • the tightness parts of Theorem 2.1 and Corollary 2.4, and the lower bounds of Theorem 2.9, which use zero-length jobs;
  • the on-line Theorem 2.8, which needs a model of on-line algorithms.
• Trivializing formalization ruled out. Dropping the optimality of $P$ from the goal would turn it into a statement about arbitrary preemptive schedules, which is Lemma 2.5, not Corollary 2.7. Comparing against $\sum_jC^P_j$ instead of every nonpreemptive schedule would likewise remove the content of the corollary.

Contributions are welcome at every level. The calculus milestone and Lemma 2.2 are good first targets.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• C. Phillips, C. Stein, J. Wein, Scheduling jobs that arrive over time, Proc. 4th Workshop on Algorithms and Data Structures (WADS), 1995, pp. 86–97 (reference [25] of the paper; no link verified).
• J. A. Hoogeveen, A. P. A. Vestjens, Optimal on-line algorithms for single-machine scheduling, Proc. 5th IPCO, 1996, pp. 404–414 (reference [21]; no link verified).
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 1997, pp. 591–598 (reference [12]; no link verified).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th FOCS, 1999 (reference [2]; no link verified).

Motivation

Facility location asks where to open service points (warehouses, plants, servers) and how to connect customers to them so that the total opening cost plus the total connection cost is minimum. In the capacitated version each facility can serve only a limited number of customers, which is the situation in most applications: a warehouse has a floor area, a server a bandwidth. The problem is NP-hard, and the algorithms used in practice for it are often simple local search heuristics: start from a solution and repeatedly apply a small change that lowers the cost, until no such change exists.

The quality of such a heuristic is measured by its locality gap: the largest possible ratio between the cost of a solution that no allowed change can improve and the cost of an optimum solution. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave locality-gap analyses for k-median, uncapacitated facility location, and the capacitated problem in which several copies of a facility may be opened. This mission formalizes their §5, the capacitated case.

Timeline (as surveyed on pp. 545–546 of the paper). For the variant 1-CFL, where at most one facility may be opened at each location, Korupolu, Plaxton and Rajaraman (1998) showed that local search with add, drop and swap moves has locality gap at most 8 when capacities are uniform; Chudak and Williamson (IPCO 1999) refined this to 6, and Pál, Tardos and Wexler gave a local search with gap 9 for nonuniform capacities. For ∞-CFL, the variant with copies studied here, the known algorithms were LP-based: a 3-approximation of Chudak and Shmoys (1999) for uniform capacities, a 4-approximation of Jain and Vazirani for nonuniform capacities, and a 2-approximation of Mahdian, Ye and Zhang. Arya et al. (2004) analysed local search for ∞-CFL with nonuniform capacities: with a new move that drops any set of open copies and opens several copies of one facility, the locality gap is at most 4 (Theorem 5.5), and scaling the facility costs gives $2 + \sqrt3 + \epsilon$ (p. 561). The tight example for uncapacitated facility location (§4.3) also shows a locally optimum solution of cost 3 times the optimum, so the locality gap of the procedure lies between 3 and 4; its exact value was left open (§6).

Setting

An instance consists of a finite set $C$ of clients, a set $F$ of facilities and a distance $c$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality; $c_{ji}$ is the cost of serving client $j$ from facility $i$. Every facility $i$ has an opening cost $f_i \ge 0$ and an integer capacity $u_i > 0$. Any number of copies of a facility may be opened; each copy of $i$ costs $f_i$ and serves at most $u_i$ clients.

A solution $X$ opens a finite list of copies, copy $s$ being a copy of facility $\mathrm{loc}(s)$, and assigns every client $j$ to a copy $\sigma(j)$ so that each copy $s$ serves at most $u_{\mathrm{loc}(s)}$ clients. Write $N_X(s)$ for the set of clients served by copy $s$ and $N_X(T)$ for the clients served by a set $T$ of copies. Its costs are

$$\mathrm{cost}_f(X) = \sum_s f_{\mathrm{loc}(s)}, \qquad \mathrm{cost}_s(X) = \sum_{j\in C} c_{j\,\mathrm{loc}(\sigma(j))}, \qquad \mathrm{cost}(X) = \mathrm{cost}_f(X) + \mathrm{cost}_s(X).$$

The neighbourhood (9) of a solution whose multiset of open facilities is $S$ consists of

1. $S + s'$: one more copy of any facility $s'$;
2. $S - T + l\cdot\{s'\}$: close any set $T$ of open copies and open $l \ge 1$ copies of a facility $s'$, provided $l\,u_{s'} \ge |N_S(T)|$.

$X$ is locally optimum if no neighbour, with any feasible assignment of the clients, has smaller cost.

Formalization targets

Goal: Theorem 5.5

For every instance with at least one client, every locally optimum solution $X$ and every solution $O$,

$$\mathrm{cost}(X) \le 4\,\mathrm{cost}(O).$$

Milestones

In the order the paper's proof uses them:

1. Lemma 5.1 (service cost): $\mathrm{cost}_s(X) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$.
2. Lemma 5.2: for every set $U$ of copies of $X$ and every facility $s'$,

$$\left\lceil \frac{|N_X(U)|}{u_{s'}}\right\rceil f_{s'} + \sum_{s\in U} |N_X(s)|\, c_{ss'} \ge \sum_{s\in U} f_s .$$

3. Lemma 5.4: in the graph with arcs $v_s \to w_o$ of length $c_{so}$ and $w_o \to \mathrm{sink}$ of length $f_o/u_o$, $|N_X(s)|$ units can be routed from every $v_s$ at cost at most $\mathrm{cost}_s(X) + \mathrm{cost}_s(O) + \mathrm{cost}_f(O)$.
4. Inequality (10): the shortest-path flow, with $T_o$ the copies routed through $w_o$, satisfies $\sum_o\sum_{s\in T_o}|N_X(s)|(c_{so} + f_o/u_o) \le \mathrm{cost}_s(X) + \mathrm{cost}_s(O) + \mathrm{cost}_f(O)$.
5. Inequality (11): $\sum_o f_o + \sum_o \sum_{s\in T_o} |N_X(s)|(c_{so} + f_o/u_o) \ge \mathrm{cost}_f(X)$.
6. Lemma 5.3 (facility cost): $\mathrm{cost}_f(X) \le 3\,\mathrm{cost}_f(O) + 2\,\mathrm{cost}_s(O)$.

A companion item states the scaled bound of p. 561: a local optimum for facility costs $(\sqrt3 - 1) f$ has cost at most $(2 + \sqrt3)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 5.5 gives a constant locality gap for a local search procedure for capacitated facility location with copies and nonuniform capacities, a variant previously approached through LP-based algorithms; the drop-add move it analyses is the paper's new operation for this problem. The scaled bound $2 + \sqrt3 \approx 3.732$ gives an approximation algorithm once local search is run to approximate local optimality. The paper also shows (Figure 13, the procedure T-hunt) that the exponentially large neighbourhood can be searched with a knapsack oracle, so the analysis applies to an implementable algorithm.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a checked model of capacitated facility location with copies (solutions, costs, the multiset neighbourhood) and of the locality-gap argument. The per-copy model and the flow comparison of Lemma 5.4 are reusable for other capacitated location problems and for local search analyses that compare a local optimum with an optimum through a flow or a matching.

Difficulty

The obvious attempt imitates the uncapacitated analysis: close one copy of $X$ and send its clients to a nearby copy of $O$. With capacities this fails, since that copy of $O$ may be too small to absorb them, and single-copy moves do not certify a constant bound. With the drop-add move a single copy of $O$ must be charged for a whole group of copies of $X$, and the groups must be chosen so that the charges add up to a constant times $\mathrm{cost}(O)$; the rounding $\lceil |N_X(T)|/u_{s'}\rceil$ of the number of new copies costs an additional $\mathrm{cost}_f(O)$ that has to be absorbed as well.

Formalization scope

• Solutions. A solution is a structure CFLSol Cl Fa u: a number n of open copies, a map loc : Fin n → Fa giving the facility of each copy, and an assignment σ : Cl → Fin n with the capacity constraint for every copy. Copies are separate indices because $N_S(s)$ is per copy. Its multiset of facilities is the image multiset of loc.
• Costs. A solution's cost is computed under its own assignment. The paper's cost of a multiset is the minimum over feasible assignments. Because every neighbour is compared with every feasible assignment, and $O$ ranges over every assignment, the statements are equivalent to the paper's. The move with $T = \{s\}$, $s' = \mathrm{loc}(s)$, $l = 1$ makes every reassignment of $X$'s clients a neighbour, so a locally optimum $X$ carries a minimum-cost assignment.
• Neighbourhood. Local optimality ranges over the whole of (9): every $s'$, every set $T$ of copies (including $\emptyset$ and all copies) and every $l \ge 1$ with $l u_{s'} \ge |N_X(T)|$. It is not restricted to what the search procedure T-hunt examines.
• Standing assumptions. Distances are nonnegative, symmetric and satisfy the triangle inequality on $C \cup F$; $d(x,x) = 0$ is not assumed. Capacities are natural numbers with $u_i > 0$; costs are real with $f_i \ge 0$; every client has unit demand. Ratios $f_o/u_o$ and the ceiling of Lemma 5.2 are computed in $\mathbb R$.
• Added hypothesis. The goal, Lemmas 5.2 and 5.3 and the companion assume at least one client. Without clients a single idle copy of a facility with $f = 1$, $u = 1$ is locally optimum at cost 1 while the empty solution costs 0, so these statements fail. The paper's instances implicitly have clients.
• No trivialization. $O$ is any solution, not a fixed optimum, and the bounds are multiplied out ($\mathrm{cost}(X) \le 4\,\mathrm{cost}(O)$, never a ratio). The empty solution is excluded only by the presence of a client, not by a default cost.
• Out of scope. The procedure T-hunt and the knapsack oracle, running time, the $\epsilon$ of approximate local optimality, and arbitrary demands.

Contributions are welcome at every level: proofs of the milestones, alternative proofs of Lemma 5.4 or (10) (for instance through a matching argument instead of flows), and general infrastructure for multiset neighbourhoods and assignment problems.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100

Motivation

A set of integers is a Sidon set if all of its pairwise sums $a+b$ ($a\le b$) are different. Sidon, in connection with Fourier analysis, asked how dense such sets can be, and the question became one of the standard problems of additive combinatorics. Let

$$h(N)=\max\{|A| : A\subseteq\{1,\dots,N\},\ A \text{ Sidon}\}.$$

A counting argument shows $h(N)\le (1+o(1))\sqrt{2N}$, and the true order was settled early: $h(N)\sim\sqrt N$. What remains open is the size of the error term $h(N)-\sqrt N$. Erdős and Turán asked whether it is smaller than every power of $N$; Erdős offered $1000 for this problem (Erdős Problem #30), and it is also Problem 31 on Green's list of open problems and problem C9 in Guy's Unsolved Problems in Number Theory.

Timeline.

• 1938 — Singer constructs, for every prime power $q$, a set of $q+1$ residues modulo $q^2+q+1$ with all differences distinct. Combined with the density of primes this gives $h(N)\ge(1-o(1))\sqrt N$ (Singer 1938).
• 1941 — Erdős and Turán prove $h(N)\le N^{1/2}+O(N^{1/4})$ (Erdős–Turán 1941).
• 1969 — Lindström gives an alternative proof with the explicit bound $h(N)\le N^{1/2}+N^{1/4}+1$ (Lindström 1969).
• 2021 — Balogh, Füredi and Roy lower the constant: $h(N)\le N^{1/2}+0.998N^{1/4}$ for large $N$ (arXiv:2103.15850).
• 2022 — O'Bryant: $h(N)\le N^{1/2}+0.99703N^{1/4}$ for large $N$ (arXiv:2207.07800).
• 2023 — Carter, Hunter and O'Bryant: $h(N)\le N^{1/2}+0.98183N^{1/4}+O(1)$, with substantial computer assistance (arXiv:2310.20032).

No upper bound with an error exponent below $1/4$ is known, and no lower bound of the form $h(N)\ge\sqrt N-O(N^{\varepsilon})$ for every $\varepsilon>0$ is known either.

Setting

A set $A$ in an additive commutative monoid is Sidon if for all $i_1,j_1,i_2,j_2\in A$,

$$i_1+i_2=j_1+j_2\ \Longrightarrow\ (i_1=j_1\wedge i_2=j_2)\ \vee\ (i_1=j_2\wedge i_2=j_1).$$

For a finite set $X$, $\operatorname{maxSidon}(X)$ is the largest size of a Sidon subset of $X$ (the empty set is Sidon, so this is well defined), and

$$h(N)=\operatorname{maxSidon}(\{1,2,\dots,N\}),\qquad h(0)=0.$$

The first values are $h(1),\dots,h(15)=1,2,2,3,3,3,4,4,4,4,4,5,5,5,5$ (OEIS A143824).

Formalization targets

Goal (Erdős Problem #30)

$$\forall\varepsilon>0:\qquad h(N)-\sqrt N = O\!\left(N^{\varepsilon}\right)\quad(N\to\infty).$$

This is a two-sided statement: it asks both for an upper bound $h(N)\le\sqrt N+C_\varepsilon N^\varepsilon$ and for a matching lower bound $h(N)\ge\sqrt N-C_\varepsilon N^\varepsilon$ for large $N$. Erdős asked it as a yes/no question; the goal fixes the conjectured answer yes, so a disproof on the platform settles the question negatively.

Milestones (known results, weakest to strongest)

1. Singer's construction: $h(q^2+q+1)\ge q+1$ for every prime power $q$.
2. Singer's lower bound: $h(N)\ge(1-\varepsilon)\sqrt N$ for every $\varepsilon>0$ and all large $N$.
3. Erdős–Turán / Lindström: $h(N)\le\sqrt N+N^{1/4}+1$ for all $N$.
4. Balogh–Füredi–Roy: $h(N)\le\sqrt N+0.998N^{1/4}$ for all large $N$.
5. O'Bryant: $h(N)\le\sqrt N+0.99703N^{1/4}$ for all large $N$.
6. Carter–Hunter–O'Bryant: $h(N)\le\sqrt N+0.98183N^{1/4}+C$ for an absolute constant $C$.

Significance

The result itself. An affirmative answer would pin $h(N)$ down to $\sqrt N$ up to a sub-polynomial error, in both directions; Erdős even speculated that $h(N)=\sqrt N+O(1)$ might hold, while remarking that this is perhaps too optimistic. A negative answer would show that the Singer-type constructions or the counting upper bounds are off by a power of $N$. Either answer would be the first change in the exponent of the error term since 1941.

Formalizing it. The goal is open. All milestones are published theorems. The platform already contains weaker related results in other formalizations (for example the order-of-magnitude bounds $c\sqrt N\le \max|A|\le\sqrt{2N}+1$ for Sidon subsets of an initial segment, and the Erdős–Turán construction); the sharp bounds listed as milestones are not stated there for this $h$. The upper bounds of Balogh–Füredi–Roy and O'Bryant are elementary but delicate optimizations, and the Carter–Hunter–O'Bryant bound relies on a large computation, so formalizing it is a substantial verification task in its own right.

Difficulty

For the upper bound, every known argument counts differences $a-a'$ in short windows and loses at the scale $N^{1/4}$; improvements since 1941 only change the constant in front of $N^{1/4}$. For the lower bound, the constructions (Singer, Bose, Ruzsa) produce Sidon sets of size about $\sqrt p$ in a modulus $p$ of size about $N$, and the loss comes from the gap between $N$ and the nearest admissible modulus; bringing it below $N^\varepsilon$ requires either new constructions or information about primes in very short intervals that is far beyond current knowledge.

Formalization scope

Sidon sets are formalized for sets in an arbitrary additive commutative monoid, with the definition, the decidability instance and $\operatorname{maxSidon}$ transcribed from the formal-conjectures library (definitions IsSidon, Finset.maxSidonSubsetCard, and Erdos30.h in FormalConjectures/ErdosProblems/30.lean), placed in the namespace Erdos30. The value $h(N)$ is a natural number cast to $\mathbb R$; $\sqrt{\cdot}$ is the real square root and $N^{\varepsilon}$, $N^{1/4}$ are real powers of $N\ge 0$. The goal's $O(\cdot)$ is Mathlib's Asymptotics.IsBigO along atTop on $\mathbb N$. The goal is not trivialized by any junk value: $h$ is a genuine finite maximum, and the $O(\cdot)$ statement concerns all large $N$.

Useful infrastructure: basic lemmas on Sidon sets (hereditary under subsets, translation invariance, distinct differences), finite projective geometry or Bose's construction for the lower bounds, and prime gaps (Bertrand's postulate suffices for $h(N)\ge c\sqrt N$ with $c<1$; a prime number theorem in short intervals is needed for $1-o(1)$). Contributions of reusable Sidon-set lemmas are welcome.

Selected references

• J. Singer, A theorem in finite projective geometry and some applications to number theory, Trans. Amer. Math. Soc. 43 (1938), 377–385. https://doi.org/10.1090/S0002-9947-1938-1501951-4
• P. Erdős and P. Turán, On a problem of Sidon in additive number theory, and on some related problems, J. London Math. Soc. 16 (1941), 212–215. https://doi.org/10.1112/jlms/s1-16.4.212
• B. Lindström, An inequality for $B_2$-sequences, J. Combin. Theory 6 (1969), 211–212. https://doi.org/10.1016/S0021-9800(69)80124-9
• J. Balogh, Z. Füredi and S. Roy, An upper bound on the size of Sidon sets, Amer. Math. Monthly (2023). https://arxiv.org/abs/2103.15850
• K. O'Bryant, On the size of finite Sidon sets (2022). https://arxiv.org/abs/2207.07800
• D. Carter, Z. Hunter and K. O'Bryant, On the diameter of finite Sidon sets (2023). https://arxiv.org/abs/2310.20032
• K. O'Bryant, A complete annotated bibliography of work related to Sidon sequences, Electron. J. Combin. DS11 (2004). https://arxiv.org/abs/math/0407117
• T. F. Bloom, Erdős Problem #30, https://www.erdosproblems.com/30
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/30.lean. https://github.com/google-deepmind/formal-conjectures

Motivation

Which sets of positive integers are forced to contain long arithmetic progressions? Van der Waerden (1927) showed that in any finite colouring of $\mathbb N$ some colour class does; Erdős and Turán (1936) asked for a density version, which became Szemerédi's theorem. Erdős then proposed the strongest natural size condition: divergence of the reciprocal sum. Erdős Problem #3 (erdosproblems.com/3) asks whether every $A\subseteq\mathbb N$ with $\sum_{n\in A}1/n=\infty$ contains arbitrarily long arithmetic progressions. Erdős attached one of his largest prizes to it. The primes are the motivating example: $\sum_p 1/p=\infty$, so a positive answer would contain the Green–Tao theorem.

Timeline.

• 1936 — Erdős and Turán conjecture that sets of positive density contain arbitrarily long progressions.
• 1953 — Roth proves the case $k=3$ of the density conjecture by Fourier analysis.
• 1975 — Szemerédi proves the density conjecture for all $k$.
• 2001 — Gowers gives the first quantitative bounds for all $k$: $r_k(N)\ll N/(\log\log N)^{c_k}$.
• 2008 — Green and Tao prove that the primes contain arbitrarily long progressions.
• 2020 — Bloom and Sisask prove $r_3(N)\ll N/(\log N)^{1+c}$, which settles the case $k=3$ of Erdős Problem #3.
• 2023 — Kelley and Meka prove $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024 — Leng, Sah and Sawhney prove $r_k(N)\le N\exp(-(\log\log N)^{c_k})$ for every $k\ge5$.

The problem is open for every $k\ge4$.

Setting

A set $S\subseteq\mathbb N$ is an arithmetic progression of length $k$ if $|S|=k$ and $S=\{a,a+d,\dots,a+(k-1)d\}$ for some $a,d\in\mathbb N$ (for $k\ge2$ the size condition forces $d>0$). For $k,N\in\mathbb N$, $r_k(N)$ denotes the largest size of a subset of $\{1,\dots,N\}$ containing no arithmetic progression of length $k$. A set $A$ has divergent reciprocal sum if $\sum_{n\in A}1/n=\infty$.

Formalization targets

Goal (Erdős Problem #3)

For every $A\subseteq\mathbb N$,

$$\sum_{n\in A}\frac1n=\infty\ \Longrightarrow\ A\ \text{contains arithmetic progressions of arbitrarily large length}.$$

This is the formal-conjectures statement erdos_3 with its answer(sorry) instantiated to the conjectured answer yes. A disproof of the goal on the platform settles the problem negatively.

Milestones

• Szemerédi's theorem for sets of positive upper density (the density case), and the existing platform statement $r_k(N)=o(N)$.
• The Green–Tao theorem (the case $A=$ primes).
• The Bloom–Sisask bound on $r_3(N)$ and its corollary, the case $k=3$ of the goal; the Kelley–Meka bound (existing platform statement).
• The Leng–Sah–Sawhney bound for $k\ge5$.
• The partial-summation reduction: bounds $r_k(N)\le N/(\log N)^{1+c_k}$ for all $k\ge3$ imply the goal.

Significance

A positive answer would be a common strengthening of Szemerédi's theorem and the Green–Tao theorem, obtained from a single size condition with no arithmetic structure. Through the reduction milestone, it is closely tied to the quantitative theory of $r_k(N)$: bounds of the shape $N/(\log N)^{1+c}$ for every $k$ would suffice. Formalizing the milestones would also give reusable Lean statements of Szemerédi-type theorems in a common language.

Difficulty

Divergence of $\sum 1/n$ is a very weak condition: such sets can have density zero, and the natural approach through $r_k(N)$ requires bounds just past $N/\log N$. For $k=3$ this barrier was only broken in 2020. For $k\ge4$ the best known bounds (Leng–Sah–Sawhney) save only a power of $\log\log N$ in the exponent, far from what is needed. The Green–Tao method uses pseudorandom majorants specific to the primes and does not apply to arbitrary sets.

Formalization scope

All statements import the published definition file Erdos142Basic, which reproduces the formal-conjectures definitions IsAPOfLengthWith, IsAPOfLength and the counting function r k N (over $\{1,\dots,N\}$). The reciprocal-sum hypothesis is ¬ Summable (fun a : A ↦ 1 / (a : ℝ)); the element $0$, if present, contributes $1/0=0$. "Arbitrarily long" is written as ∃ᶠ k in atTop, which is equivalent to "every length" because sub-progressions of progressions are progressions. Bounds stated in the literature with $\ll$ are written without a multiplicative constant and with "for all sufficiently large $N$"; the constant can be absorbed into the exponent. Contributions formalizing partial summation over sets of naturals and the equivalence of the "frequently" and "for every $k$" forms are welcome.

Selected references

• P. Erdős and P. Turán, On some sequences of integers, J. London Math. Soc. 11 (1936).
• K. F. Roth, On certain sets of integers, J. London Math. Soc. 28 (1953).
• E. Szemerédi, On sets of integers containing no k elements in arithmetic progression, Acta Arith. 27 (1975).
• W. T. Gowers, A new proof of Szemerédi's theorem, Geom. Funct. Anal. 11 (2001).
• B. Green and T. Tao, The primes contain arbitrarily long arithmetic progressions, Ann. of Math. 167 (2008).
• T. F. Bloom and O. Sisask, Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions, arXiv:2007.03528 (2020).
• Z. Kelley and R. Meka, Strong bounds for 3-progressions, FOCS 2023, arXiv:2302.05537.
• J. Leng, A. Sah and M. Sawhney, Improved bounds for Szemerédi's theorem, arXiv:2402.17995 (2024).
• T. F. Bloom, Erdős Problem #3, https://www.erdosproblems.com/3

Motivation

Addition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.

Timeline.

• 1983 — Erdős and Szemerédi show that $\max(|A+A|,|AA|)\ge c|A|^{1+\delta}$ for some absolute $\delta>0$ and every finite set of integers $A$, and conjecture exponent $2-\varepsilon$.
• 1997 — Nathanson obtains the explicit exponent $1+\tfrac1{31}$; Ford (1998) improves it to $1+\tfrac1{15}$.
• 1997 — Elekes, using the Szemerédi–Trotter incidence theorem, proves $|A+A|\,|AA|\gg|A|^{5/2}$ for finite sets of reals, hence exponent $5/4$.
• 2009 — Solymosi proves $|A+A|^2|AA|\gg |A|^4/\log|A|$ for finite sets of positive reals, hence exponent $4/3$ up to a logarithmic factor.
• 2015–2022 — Konyagin and Shkredov first break the $4/3$ barrier (exponent $4/3+c$ for a small explicit $c>0$); after several improvements, Rudnev and Stevens reach $4/3+2/1167$ up to logarithmic factors.

The conjecture itself remains open.

Setting

For a finite set $A\subset\mathbb Z$ define the sumset and product set

$$A+A=\{a+b : a,b\in A\},\qquad AA=\{ab : a,b\in A\}.$$

For nonempty $A$ both contain at least $|A|$ elements and at most $\binom{|A|+1}{2}$. The quantity of interest is $\max(|A+A|,|AA|)$ as a function of $|A|$.

Formalization targets

Goal (Erdős–Szemerédi conjecture)

For every $0<\varepsilon<1$ there is $C_\varepsilon>0$ such that for every finite set $A\subset\mathbb Z$,

$$\max(|A+A|,|AA|)\ \ge\ C_\varepsilon\,|A|^{2-\varepsilon}.$$

Known lower bounds (milestones, weakest to strongest)

$$|A+A|\ge 2|A|-1,\qquad \max(|A+A|,|AA|)\gg|A|^{1+\delta},\qquad \gg|A|^{5/4},\qquad \gg\frac{|A|^{4/3}}{(\log|A|)^{1/3}},\qquad \gg_\varepsilon |A|^{4/3+2/1167-\varepsilon}.$$

Sharpness

The $\varepsilon$ cannot be removed: there is no $C>0$ with $\max(|A+A|,|AA|)\ge C|A|^2$ for all $A$ (take $A=\{1,\dots,n\}$; the multiplication table $|AA|$ is $o(n^2)$ by Erdős).

Significance

A proof of the goal would settle the sharp form of the sum–product phenomenon over $\mathbb Z$. Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over $\mathbb R$ have come together with new incidence-geometric tools.

Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.

Difficulty

Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near $4/3$, and passing beyond $4/3$ has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to $2$; even over $\mathbb Z$, where arithmetic structure is available, the best general bounds are the real-number ones.

Formalization scope

Sets are Finset ℤ; $A+A$ and $AA$ are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to $\mathbb R$. Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis $\varepsilon<1$ keeps every exponent positive, so the empty set contributes the trivial inequality $0\ge 0$ rather than a junk value $0^0=1$. The constant $C$ may depend on $\varepsilon$ but not on $A$. The Solymosi milestone is stated for $|A|\ge2$ so that $\log|A|>0$.

The statements are for integer sets only; results proved over $\mathbb R$ specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over $\mathbb R$, multiplicative energy, bounds for the multiplication table) are welcome.

Selected references

• P. Erdős, E. Szemerédi, On sums and products of integers, Studies in Pure Mathematics, Birkhäuser, 1983, 213–218.
• M. B. Nathanson, On sums and products of integers, Proc. Amer. Math. Soc. 125 (1997), 9–16.
• K. Ford, Sums and products from a finite set of real numbers, Ramanujan J. 2 (1998), 59–66.
• G. Elekes, On the number of sums and products, Acta Arith. 81 (1997), 365–367.
• J. Solymosi, Bounding multiplicative energy by the sumset, Adv. Math. 222 (2009), 402–408. https://arxiv.org/abs/0806.1040
• S. V. Konyagin, I. D. Shkredov, On sum sets of sets having small product set, Proc. Steklov Inst. Math. 290 (2015), 288–299. https://arxiv.org/abs/1503.05771
• M. Rudnev, S. Stevens, An update on the sum-product problem, Math. Proc. Cambridge Philos. Soc. 173 (2022), 411–430. https://arxiv.org/abs/2005.11145
• Erdős Problem 52, https://www.erdosproblems.com/52