All missions

Motivation

Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).

Timeline (as recounted on pp. 2–3 of the source):

• 2004: Lipton, Markakis, Mossel and Saberi introduce the envy-graph and cycle-elimination technique and compute allocations now called EF1 (DOI 10.1145/988772.988792).
• 2016: Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang define EFX (DOI 10.1145/2940716.2940726).
• 2018: Plaut and Roughgarden prove EFX allocations of all goods exist for two agents, or for any number of agents with identical valuations (arXiv:1707.04769).
• 2019: Caragiannis, Gravin and Huang introduce EFX with charity: a partial EFX allocation in which each agent gets at least half her value in a Nash-optimal allocation, with no bound on the number or value of donated goods (arXiv:1902.04319).
• 2020: Chaudhury, Garg and Mehlhorn prove existence of complete EFX allocations for three agents with additive valuations (arXiv:2002.05119).
• 2020/2021: the present paper bounds the charity: fewer goods than unenvied agents, and no agent envies the donated set. Its SODA 2020 version assumed gross-substitute valuations; the journal version (arXiv v3) needs only normalized monotone valuations (p. 8, §1.4).

The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.

Setting

There are $n\ge1$ agents, indexed by $N=\{1,\ldots,n\}$ in the paper, and a finite set $M$ of $m$ indivisible goods. Agent $i$ has a valuation $v_i:2^M\to\mathbb R_{\ge0}$. It is normalized if $v_i(\varnothing)=0$ and monotone if $S\subseteq T$ implies $v_i(S)\le v_i(T)$. No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.

A partial allocation $X=(X_i)_{i\in N}$ consists of pairwise disjoint bundles $X_i\subseteq M$. Its pool is the goods not assigned to anyone,

$$P(X)=M\setminus\bigcup_{i\in N}X_i.$$

The allocation is EFX when

$$v_i(X_j\setminus\{g\})\le v_i(X_i) \qquad\text{for all }i,j\in N\text{ and every }g\in X_j.$$

The paper calls allocations partial by default (p. 3, footnote 5). The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ when $v_i(X_i)<v_i(X_j)$. A source is a vertex with no incoming edge. Its reachability component $C(s)$ includes $s$ itself. The social welfare of $X$ is $\phi(X)=\sum_i v_i(X_i)$. These notions are introduced on pp. 8–9 of the source.

For a set $S$ of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset $Z$ is envied, but no strict subset of $Z$ is envied by anyone. An agent who envies such a $Z$ is a most envious agent of $S$; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).

Formalization targets

The goal is the allocation guarantee of Theorem 8:

$$\exists X\text{ partial}:\quad X\text{ is EFX},\qquad v_i(P(X))\le v_i(X_i)\ (i\in N),\qquad |P(X)|<|\operatorname{sources}(G_X)|\le n.$$

Both the stronger source-count bound and its consequence $|P(X)|<n$ are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.

The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if $X$ is EFX then $X'$ is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.

Significance

The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).

The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.

Difficulty

EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.

Formalization scope

Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis $n>0$ is explicit because the paper presumes agents and the strict bound $|P|<n$ is false when $n=0$. The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair $i,j$, including $i=j$, and every good of $X_j$.

The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold $|P|\ge n$ with $|P|\ge|\operatorname{sources}(G_X)|$, the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.

The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an $nmV/\Delta$ iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, arXiv:1907.04596v3, 2020; published in SIAM Journal on Computing, 2021. Pinned preprint.
• R. J. Lipton, E. Markakis, E. Mossel and A. Saberi, On approximately fair allocations of indivisible goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah and J. Wang, The unreasonable fairness of maximum Nash welfare, ACM EC 2016. https://doi.org/10.1145/2940716.2940726
• B. Plaut and T. Roughgarden, Almost envy-freeness with general valuations, SODA 2018. https://arxiv.org/abs/1707.04769
• I. Caragiannis, N. Gravin and X. Huang, Envy-freeness up to any item with high Nash welfare: the virtue of donating items, ACM EC 2019. https://arxiv.org/abs/1902.04319
• B. R. Chaudhury, J. Garg and K. Mehlhorn, EFX exists for three agents, ACM EC 2020. https://arxiv.org/abs/2002.05119

Motivation

Many scheduling decisions are not owned by a single decision maker. A machine shared by two departments, a production line serving two customers, or a computing resource shared by two users must process the jobs of two agents, each of which judges a schedule by its own criterion. Agnetis, Mirchandani, Pacciarelli and Pacifici introduced this model in Scheduling Problems with Two Competing Agents (Operations Research, 2004, doi:10.1287/opre.1030.0092), and it became the starting point of the literature on multi-agent scheduling (surveyed in Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer, 2014, doi:10.1007/978-3-642-41880-8).

When neither agent can impose its criterion on the other, the natural object to compute is the set of compromises that cannot be improved for one agent without hurting the other: the Pareto frontier. Section 11 of the paper asks how large that frontier can be for each pair of criteria it studies, because the size of the frontier decides whether it can be listed in polynomial time. This mission formalizes the answer for one agent minimizing its total completion time against the other agent's maximum cost.

Setting

Agent $A$ owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent $B$ owns jobs $J^B_1,\dots,J^B_{n_B}$, with $n_B\ge 1$. Every job $J_j$ has a positive processing time $p_j$, is available at time $0$, and is processed without interruption on a single machine that handles one job at a time. Since both criteria below are nondecreasing in completion times, a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed in that order from time $0$ without idle time, and $C_j(\sigma)$ denotes the completion time of $J_j$.

• Agent $A$ wants to minimize its total completion time $\sum_{h=1}^{n_A} C^A_h(\sigma)$.
• Each $B$-job has a nondecreasing cost function $f^B_k$ of its completion time, and agent $B$ wants to minimize its maximum cost $f^B_{\max}(\sigma)=\max_k f^B_k(C^B_k(\sigma))$.

A schedule $\sigma$ is nondominated if no schedule $\bar\sigma$ has $\sum C^A_h(\bar\sigma)\le\sum C^A_h(\sigma)$ and $f^B_{\max}(\bar\sigma)\le f^B_{\max}(\sigma)$ with at least one inequality strict. Its nondominated pair is $\bigl(\sum C^A_h(\sigma),f^B_{\max}(\sigma)\bigr)$. The constrained problem $1\|\sum C^A_i : f^B_{\max}\le Q$ asks for a schedule with $f^B_k(C^B_k)\le Q$ for every $B$-job that minimizes $\sum C^A_h$ among such schedules; such a schedule is optimal for the bound $Q$.

The $A$-jobs of a schedule follow the SPT order when they appear by nondecreasing processing time, equal lengths in index order. A $B$-job overtakes an $A$-job when it moves from after it to before it.

Formalization targets

Goal: Theorem 11.6, corrected

$$\bigl|\{(\textstyle\sum C^A_h(\sigma),\,f^B_{\max}(\sigma)) : \sigma\ \text{nondominated}\}\bigr|\ \le\ n_A\,n_B+1.$$

The paper prints the bound $n_An_B$. That bound is false: with one job per agent, unit processing times and $f^B(t)=t$, the schedules $AB$ and $BA$ give the two nondominated pairs $(1,2)$ and $(2,1)$. The corrected bound $n_An_B+1$ is the one the printed argument supports.

Milestones

1. Lemma 5.4 (p. 234): if no $B$-job can complete last within the bound, every optimal schedule ends with a longest $A$-job. This is the reason the $A$-jobs of optimal schedules are in SPT order.
2. Lemma 11.4 (p. 240): for $Q'<Q$ and optimal schedules $\sigma,\sigma'$ for $Q$ and $Q'$ whose $A$-jobs follow the SPT order, $C_j(\sigma')\ge C_j(\sigma)$ for every $A$-job $j$.
3. Lemma 11.5 (p. 240): under the same hypotheses, if a $B$-job precedes an $A$-job in $\sigma$, it precedes it also in $\sigma'$.

Significance

A frontier of size at most $n_An_B+1$ means that the scheme the paper calls PP, which solves the constrained problem for a decreasing sequence of bounds, lists every nondominated pair with polynomially many calls to a polynomial algorithm (Theorem 5.5 of the paper). The contrast with the other criteria of §11 is the point: for two total-completion-time agents the paper exhibits an exponential frontier (Example 11.7). The bound therefore separates criteria whose compromises can be negotiated over an explicit list from those where they cannot.

Formalizing it adds three things. First, the printed statements need corrections: the bound is off by one, and Lemmas 11.4 and 11.5 are false when identical $A$-jobs may be ordered differently in the two schedules. A machine-checked version fixes the exact hypotheses. Second, the monotonicity of overtakes (Lemma 11.5) is a reusable structural fact about parametric scheduling under a tightening constraint. Third, no part of this paper or of two-agent scheduling has been machine-checked before, to our knowledge; the published sequence model the mission builds on comes from the formalization of Moore's 1968 algorithm.

Difficulty

The obvious argument counts overtakes: as the bound decreases, each $B$-job overtakes each $A$-job at most once, so consecutive frontier points differ by at least one new overtake. The step that does not go through as printed is "at most once". Optimal schedules for a given bound are not unique, and two optimal schedules can disagree on the order of identical $A$-jobs and on the position of a $B$-job between them. Then an "overtake" can be undone between two bounds without any change in the objectives. The counting is valid only for a consistently chosen family of schedules, and turning the comparison of optimal schedules for two different bounds into a strict improvement needs an exchange argument with careful bookkeeping of which jobs shift. A second, smaller gap is the base case: the first schedule of the chain carries no overtake and must be counted separately.

Formalization scope

Jobs are Fin nA ⊕ Fin nB, 0-based, and a schedule is a duplicate-free list of all jobs; completion times come from the published definition MooreLateJobs.Shared.completionTime (Moore 1968 series), referenced rather than redefined. Processing times are real and strictly positive, the paper's standing convention, which the exchange arguments use. The bound $Q$ is real; the paper's integer $Q$ is a special case. Feasibility for the bound is stated job by job. The maximum cost $f^B_{\max}$ is a finite maximum and requires $n_B\ge 1$.

Explicit readings of the paper's phrases:

• "Nondominated schedules" in Theorem 11.6 is read as nondominated pairs, one schedule per pair, as §11 defines the set it enumerates. Counting schedules would count swaps of identical jobs separately.
• The count is Set.encard of a set of real pairs, so the goal asserts finiteness as well as the bound; it is not a Set.ncard, which would be $0$ on an infinite set.
• "The $A$-jobs are always SPT ordered" (p. 240) is read as the SPT order with ties broken by index, imposed as a hypothesis on both schedules in Lemmas 11.4 and 11.5. Without a fixed tie-break both lemmas are false.
• Lemma 5.4 is restated with $n_A\ge 1$, since an empty schedule has no last job. It is also a milestone of mission 3 of this series and is restated here identically because draft items cannot import each other.

Nothing in the statements is trivial by construction. The goal is about every instance with positive data, its hypotheses are satisfiable, and the counterexample to the printed bound is checked in Lean. The milestones' SPT hypotheses are met by some optimal schedule of every feasible instance, so they are not vacuous. Running times, including the polynomiality of PP and the choice of the decrement $\epsilon$ in Figure 4, are not formalized.

A complete development needs exchange lemmas for single-machine sequences (moving a job, swapping two adjacent jobs, and their effect on completion times), the existence of SPT-ordered optimal schedules, and a chain-counting argument for nested sets of overtakes. The exchange lemmas are reusable for any single-machine sequencing mission. Contributions of any of these, and of a proof of the corrected bound that avoids the scheme PP, are welcome.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2), 229–242, 2004. https://doi.org/10.1287/opre.1030.0092
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1), 102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer, 2014. https://doi.org/10.1007/978-3-642-41880-8

Motivation

Many scheduling situations involve more than one decision maker sharing a resource. Two departments of a firm may share a machine shop, two clients may share a contractor, or two users may share a processor, and each cares only about how its own jobs are served. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced a systematic study of such two-agent scheduling problems. Their framework has two questions. The constrained problem asks for the best schedule for one agent among those that keep the other agent's cost below a bound. The Pareto problem asks for the schedules whose cost pair cannot be improved for one agent without hurting the other. The paper settles the complexity of these questions for the standard scheduling objectives and gave rise to a large literature on multi-agent scheduling (see the survey by Perez-Gonzalez and Framinan, EJOR 235, 2014).

This mission covers §5.2 of the paper: agent $A$ minimizes the total completion time of its jobs, and agent $B$ requires that the maximum of its jobs' regular costs stay below a bound $Q$.

Setting

Agent $A$ owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent $B$ owns jobs $J^B_1,\dots,J^B_{n_B}$. Job $J_j$ has a processing time $p_j>0$. All jobs are available at time $0$ and are processed one at a time, without interruption, on a single machine. Because every objective here is nondecreasing in the completion times, the machine is never left idle, and a schedule $\sigma$ is simply a sequence of all $n_A+n_B$ jobs; the completion time $C_j(\sigma)$ of a job is the total processing time of that job and the jobs before it. Write $P_A$ and $P_B$ for the total processing times of the two agents.

Agent $A$'s objective is the total completion time $\sum_h C^A_h(\sigma)$. Each $B$-job has a nondecreasing cost function $f^B_k$, and agent $B$'s objective is the maximum cost

$$f^B_{\max}(\sigma)=\max_k f^B_k\bigl(C^B_k(\sigma)\bigr).$$

Given a bound $Q$, a schedule is feasible for the problem $1\|\sum C^A_i : f^B_{\max}\le Q$ if $f^B_k(C^B_k)\le Q$ for every $B$-job, and optimal if it is feasible and minimizes $\sum C^A_h$ among feasible schedules. The instance is feasible if a feasible schedule exists. A schedule is nondominated if no schedule is at least as good for both agents and strictly better for one.

The paper solves the problem with a backward rule (Figure 1). Fill the sequence from the end. With $\tau$ the total length of the jobs not yet placed, place last any unplaced $B$-job with $f^B_k(\tau)\le Q$. If there is none, place last a longest unplaced $A$-job. If neither exists, the instance is infeasible. The least-cost variant of §5.2.1 chooses, among the $B$-jobs, one minimizing $f^B_k(\tau)$ over all unplaced $B$-jobs. A B-block of a schedule is a maximal run of consecutive $B$-jobs.

Formalization targets

Goal: Theorem 5.7

On a feasible instance with $n_B\ge1$, every schedule $\tilde\sigma$ produced by the least-cost variant, under any tie-breaking, satisfies

$$\tilde\sigma \text{ is optimal for } 1\|\textstyle\sum C^A_i : f^B_{\max}\le Q \quad\text{and}\quad \tilde\sigma \text{ is nondominated for } \bigl(\textstyle\sum C^A_i,\ f^B_{\max}\bigr).$$

The nondominance is the printed theorem; the optimality is how the paper introduces $\tilde\sigma$, and rests on Theorem 5.5.

Milestones

• Lemma 5.3: if some $B$-job $J^B_{\bar k}$ has $f^B_{\bar k}(P_A+P_B)\le Q$, some optimal schedule ends with $J^B_{\bar k}$ and no optimal schedule ends with an $A$-job.
• Lemma 5.4: if every $B$-job has $f^B_k(P_A+P_B)>Q$, every optimal schedule ends with a longest $A$-job.
• Theorem 5.5 (correctness): on a feasible instance every schedule of Figure 1 is optimal, and Figure 1 runs to completion exactly on feasible instances.
• Lemma 5.6: all optimal schedules have the same partition of the $B$-jobs into B-blocks, and each B-block occupies the same time interval in all of them.

Significance

Theorem 5.5 shows that the constrained problem with total completion time against a maximum cost is solvable by sorting, in contrast to its weighted version, which the same section shows NP-hard. Lemma 5.6 describes all optimal schedules: they agree on the completion times of the $A$-jobs (up to permuting identical jobs) and on the B-blocks, and differ only inside each block. Theorem 5.7 turns this into a nondominated schedule. It is the building block for the Pareto problem $1\|\sum C^A_i\circ f^B_{\max}$ of §11.2, where solving the constrained problem for a sequence of bounds enumerates the nondominated pairs.

The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission formalizes the statements and asks for their proofs. The proof of Theorem 5.7 invokes "the very same proof of Lawler's algorithm (Lawler 1973) restricted to $1\|f_{\max}$", applied inside each B-block. Lawler's rule is a separate statement on the platform, LawlerPrec.MinMax.lawler_rule_optimal, currently open. A solver may prove it and adapt it, but the goal does not need it in that exact form.

Difficulty

The interchange arguments of Lemmas 5.3 and 5.4 are short. The obstacle is Lemma 5.6. Two optimal schedules can differ in which $B$-job is placed at each step, and in the order of $A$-jobs of equal length. The paper's argument compares the completion time of each $A$-job across two optimal schedules and shows it cannot move earlier. That needs the fact that a $B$-job finishing before an $A$-job could not have been placed at that $A$-job's completion time, which comes from applying Lemma 5.3 to a prefix of the schedule. Formalizing it requires restricting optimality to prefixes and sub-instances, which the bare sequence model does not provide. The tempting shortcut of proving Theorem 5.7 from Lawler's rule on the whole schedule fails, since the bound $Q$ and agent $A$'s objective change which jobs may be placed where; the reduction is only to one Lawler instance per block.

Formalization scope

Jobs are Fin nA ⊕ Fin nB (0-based). A schedule is a duplicate-free list of all jobs, with completion times from the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968 series), which this mission reuses. Processing times are real and strictly positive. Without positivity the second claim of Lemma 5.3 fails, because a zero-length $B$-job can sit anywhere. Cost functions are real-valued and nondecreasing, and $Q$ is real (the paper's integer $Q$ is a special case). Feasibility is stated job by job; $f^B_{\max}$ is a finite maximum and requires $n_B\ge1$, which the goal assumes. Lemma 5.4 assumes $n_A\ge1$, since "a longest $A$-job" presupposes one.

The paper's loose phrases are read as follows:

• "the algorithm" is a property of a finished sequence. At position $m$, with the jobs at positions $0,\dots,m$ unplaced and $\tau$ their total length, the job at $m$ must be a choice the rule allows.
• "Ties are broken arbitrarily" means that every sequence satisfying the rule is covered.
• "no solution exists, STOP" leaves no allowed choice. Running to completion therefore means that some sequence satisfies the rule.
• "the optimal schedule generated in this way" puts optimality into the goal as a conclusion, not a hypothesis.
• "a longest A-job" is an $A$-job of maximal length; when several are tied, no statement fixes which one.
• Nondominance quantifies over all schedules, not only those feasible for $Q$.
• A B-block's interval runs from the earliest start to the latest completion of its jobs.

The running times of Theorems 5.5 and 5.8 ($O(n_A\log n_A+n_B\log n_B)$ and $O(n_A\log n_A+n_B^2)$) are not formalized. Nor is the claim (3) inside the proof of Lemma 5.6.

A trivializing formalization is ruled out: feasibility of the instance is a hypothesis and not built into the rule, the rule constrains every position, and the goal asserts nondominance against all schedules.

Useful infrastructure includes interchange lemmas for the sequence model (moving one job to the end, swapping two jobs), restriction of a schedule to a prefix, and Lawler's rule for $1\|f_{\max}$ on a fixed time window. The interchange lemmas and the prefix restriction are reusable across the whole two-agent series.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2), 229–242, 2004. https://doi.org/10.1287/opre.1030.0092
• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1), 102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and Approximation in Deterministic Sequencing and Scheduling: A Survey, Annals of Discrete Mathematics 5, 287–326, 1979. https://doi.org/10.1016/S0167-5060(08)70356-X
• P. Perez-Gonzalez, J. M. Framinan, A common framework and taxonomy for multicriteria scheduling problems with interfering and competing jobs: Multi-agent scheduling problems, European Journal of Operational Research 235(1), 1–16, 2014. https://doi.org/10.1016/j.ejor.2013.09.017

Motivation

Steepest descent is the oldest method for unconstrained minimization: to minimize a smooth function $f$, it moves from the current point $x_k$ along the negative gradient $-g_k = -\nabla f(x_k)$. It is the prototype of every first-order method, and its worst-case evaluation complexity — how many iterations it may need before the gradient norm drops below a tolerance $\epsilon$ — is the reference point against which faster methods are measured.

For a function that is bounded below and has a Lipschitz continuous gradient, steepest descent with a suitable step-length rule reaches $\|g_k\| \le \epsilon$ within $O(\epsilon^{-2})$ iterations (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Whether this bound is tight on nonconvex problems remained open until Cartis, Gould and Toint (preprint 15 October 2009; SIAM J. Optim. 20(6), 2010) built explicit one-dimensional examples showing that it is essentially sharp. The same paper shows that Newton's method can be as slow, and that the $O(\epsilon^{-3/2})$ bound of cubically regularized Newton methods is also tight; those results are the other missions of this series.

Timeline:

• 1983: Dennis and Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, Theorem 6.3.3 — global convergence of steepest descent with a Goldstein–Armijo linesearch under twice continuous differentiability, boundedness below and a Lipschitz gradient.
• 2004: Nesterov's textbook states the $O(\epsilon^{-2})$ iteration bound for gradient methods on nonconvex functions with Lipschitz gradient.
• 2009/2010: Cartis, Gould and Toint construct, for every $\tau > 0$, examples on which steepest descent needs at least $\lfloor \epsilon^{-(2-\tau)} \rfloor$ iterations.

Setting

Let $f : \mathbb R \to \mathbb R$ be twice continuously differentiable, bounded below, with a derivative $f'$ that is bounded and Lipschitz continuous. The paper calls these standing assumptions AS.0. Write $g(x) = f'(x)$ for the gradient.

Steepest descent with step lengths $(\alpha_k)_{k\ge0}$ starts at $x_0 = 0$ and sets

$$x_{k+1} = x_k - \alpha_k\, g(x_k), \qquad k \ge 0.$$

The step lengths are only required to lie in a fixed interval (condition (2.6))

$$0 < \underline\alpha \le \alpha_k \le \overline\alpha < 2 .$$

Such step lengths can be produced by a Goldstein–Armijo linesearch, which accepts a step when the decrease $f(x_k) - f(x_{k+1})$ lies between $a\,\alpha_k|g_k|^2$ and $b\,\alpha_k|g_k|^2$ for fixed constants $0 < a < b < 1$.

Fix $\tau \in (0,1)$ and put $\eta = \eta(\tau) = \frac{1}{2-\tau} - \frac12 = \frac{\tau}{4-2\tau}$. The mission's definitions (namespace SlowConvergence.SteepestDescent) record the paper's prescribed data: iterates xk, steps sk, values fk, gradients $g_k = -(1/(k+1))^{\frac12+\eta}$ (gk), and the quintic pieces p with the quantities $\psi_k$, $\phi_k$, $\mu_k$ of (2.11)–(2.15).

Formalization targets

Goal: steepest descent can need $\lfloor \epsilon^{-(2-\tau)}\rfloor$ iterates

For every $\tau \in (0,1)$, every $0 < \underline\alpha \le \overline\alpha < 2$ and every step-length sequence with $\underline\alpha \le \alpha_k \le \overline\alpha$, there is $f$ satisfying AS.0 on all of $\mathbb R$ on which the steepest descent run from $x_0 = 0$ has

$$|f'(x_k)| = \Big(\frac{1}{k+1}\Big)^{\frac{1}{2-\tau}} \quad (k \ge 0), \qquad\text{hence}\qquad |f'(x_k)| \le \epsilon < 1 \;\Longrightarrow\; k+1 \ge \Big\lfloor \frac{1}{\epsilon^{2-\tau}} \Big\rfloor .$$

No constant (Lipschitz constant, gradient bound, lower bound) is fixed in the goal; only its existence is asserted.

Milestones

1. (2.10) and (2.3): $\eta > 0$ and $|g_k| = (1/(k+1))^{1/(2-\tau)}$.
2. The Goldstein–Armijo remark (p. 4): for $2(1-b) \le \alpha_k \le 2(1-a)$ the prescribed decrease satisfies both linesearch conditions.
3. (2.12)–(2.14): the quintic $p_k$ meets its six Hermite conditions on $[0,\mu_k]$.
4. (2.15): $0 < \psi_k < 1$.
5. (2.17): $|p_k''(t)| \le 1 + 150|\phi_k| \le 1 + 150\max[1,\overline\alpha]/\underline\alpha$ on $[0,\mu_k]$.
6. Lower bound (p. 5): $f_k - f_{k+1} \le \frac12 (1/(k+1))^{1+2\eta}$ and $f_k \ge 0$.

Significance

The result. Since $\tau > 0$ is arbitrary, the example shows that the $O(\epsilon^{-2})$ upper bound for steepest descent cannot be improved to $O(\epsilon^{-2+\tau})$ for any $\tau > 0$ under AS.0, even with a standard Goldstein–Armijo linesearch. It separates steepest descent from second-order methods with better worst-case bounds, and it is the template for the Newton and regularized-Newton examples of the same paper. A matching upper bound for gradient descent with step $1/L$ is formalized elsewhere on the platform (ShiOptRates.gd_exact_rate); together the two describe the complexity of the method up to the exponent $\tau$.

Formalizing it. The result is proved on paper; to our knowledge no machine-checked version exists. The mission adds a statement in which the method, the function class and the iteration count are fixed precisely. It also corrects three printed slips that a formal check exposes: the iteration count is off by one, the Goldstein–Armijo interval is printed reversed, and an intermediate step of (2.17) is false while its end bounds hold.

Difficulty

Matching prescribed values $f_k$ and gradients $g_k$ at the iterates is easy one point at a time. The difficulty is doing it with uniform control. The interval lengths $\mu_k$ shrink like $(k+1)^{-1/(2-\tau)}$, so a naive interpolant has second derivatives growing with $k$, and the gradient is then not globally Lipschitz. The prescribed values must also decrease at a rate whose sum stays finite, or the function is unbounded below. Both constraints pin the exponent: the construction works only because $\frac12 + \eta < 1$ makes the iterates escape to infinity while $1 + 2\eta > 1$ keeps $\sum_k (f_k - f_{k+1})$ finite. A further step remains: the paper's function lives on $[0,\infty)$ and must be extended to all of $\mathbb R$ without losing any property of AS.0.

Formalization scope

The problem is one-dimensional: f : ℝ → ℝ, the gradient is deriv f, and the second derivative is iteratedDeriv 2. AS.0 is ContDiff ℝ 2 f, BddBelow (Set.range f), a global bound on |deriv f|, and LipschitzWith L (deriv f). Every property holds on all of $\mathbb R$; the paper constructs $f$ on $[0,\infty)$ and says it extends smoothly to the negative reals, and that extension is part of the goal.

Conventions:

• $\tau \in (0,1)$: the construction needs it, and for $\epsilon < 1$ smaller $\tau$ gives larger counts, so the paper's "any $\tau > 0$" follows.
• The count is $k + 1 \ge \lfloor \epsilon^{-(2-\tau)} \rfloor$ (natural floor), the number of iterates $x_0, \dots, x_k$; the printed "iterations" count $k$ is off by one.
• Exponents are Real.rpow with base $1/(k+1) > 0$.
• The real zeta function is the series $\sum_{n\ge0} (1/(n+1))^t$, used only at $t = 1 + 2\eta > 1$.
• The step lengths are universally quantified before $f$, and the steepest-descent run is part of the conclusion, tied to $f$ by $x_{k+1} = x_k - \alpha_k f'(x_k)$. A goal asserting slow gradients along some sequence unrelated to $f$, or for one convenient step-length sequence only, would be trivial or weaker and is not the statement.

Infrastructure needed: quintic Hermite interpolation on intervals, gluing piecewise polynomials into a $C^2$ function on $[0,\infty)$ along an unbounded increasing knot sequence, a $C^2$ extension to the negative reals, and bounds for real $p$-series. The gluing lemma and the extension are reusable for the Newton and regularized-Newton missions of the series. Contributions of any milestone, of a construction of the glued function $f_1$ of (2.16), or of a direct proof of the goal are welcome.

Selected references

• C. Cartis, N. I. M. Gould, Ph. L. Toint, On the complexity of steepest descent, Newton's and regularized Newton's methods for nonconvex unconstrained optimization problems, SIAM J. Optim. 20(6), 2833–2852, 2010. https://doi.org/10.1137/090774100 (preprint 15 Oct 2009: https://people.maths.ox.ac.uk/cartis/papers/cgt36.pdf)
• J. E. Dennis, R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, Prentice-Hall, 1983. https://doi.org/10.1137/1.9781611971200
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Quasi-Newton methods replace a costly exact Hessian with an operator updated from successive changes in position and gradient. A secant update must map the observed step $s$ to the observed gradient difference $y$. Many operators satisfy that one equation, so the choice of update needs another criterion. Gilbert and Lemaréchal's working paper studies variable-storage quasi-Newton algorithms and, in its Annex, characterizes familiar update formulas by how little they change the previous operator. The Annex treats real Hilbert spaces, rather than only matrices on Euclidean space, and allows the underlying scalar product and the weighting operator to vary. Its least-change characterization is the subject of this mission.

The source is the August 1988 IIASA Working Paper WP-88-121. A revised journal article appeared in 1989, but the theorem numbers and printed page references here belong to the working paper. The work is a formalization of a result proved in that paper; the mathematical question is not open.

Setting

Let $\mathcal H$ be a complete real inner-product space. A continuous linear operator $B$ is the current Hessian approximation. A step $s\in\mathcal H$ and a gradient difference $y\in\mathcal H$ determine the quasi-Newton equation $B_+s=y$ for the updated operator $B_+$. Write $B_+=B+P$, where $P$ is the perturbation. The source restricts $P$ to the Hilbert–Schmidt class $L_2(\mathcal H)$, so its size can be measured by an orthonormal basis $(e_i)_{i\in I}$:

$$\|P\|_{\mathrm{HS}}=\left(\sum_{i\in I}\|Pe_i\|^2\right)^{1/2}.$$

The index set $I$ need not be countable; membership in $L_2(\mathcal H)$ means the displayed family is summable. The value is independent of the chosen orthonormal basis. For $u,v\in\mathcal H$, the paper's bracket operator is $[u,v]d=\langle v,d\rangle u$. The order of its arguments matters.

The nonsymmetric feasible set is $\Pi=\{P\in L_2(\mathcal H):(B+P)s=y\}$. For a self-adjoint $B$, the symmetric problem uses $\Pi_S=\{P\in L_2(\mathcal H):P=P^*,\ (B+P)s=y\}$. A bijective continuous operator $R$ weights the symmetric objective $\|R^*PR\|_{\mathrm{HS}}$. The vector $c=R^{-*}R^{-1}s$ records how this weight changes the update. Both the feasible set and the weighted objective matter: taking a minimum over every bounded operator would change the problem.

Formalization targets

The goal is Proposition A.2 on printed p. 28 of the working paper. Suppose $B=B^*$, $R$ is bijective, and $s\ne0$. With $r=y-Bs$ and $c=R^{-*}R^{-1}s$, define

$$P_c=\frac{[r,c]+[c,r]}{\langle c,s\rangle} -\frac{\langle r,s\rangle}{\langle c,s\rangle^2}[c,c].$$

The target asserts that $P_c$ belongs to $\Pi_S$ and is the unique minimizer of $\|R^*PR\|_{\mathrm{HS}}$ over $P\in\Pi_S$. Its formula depends on $R$ only through $c$. No positivity condition on $B$ or on $\langle y,s\rangle$ is part of this result.

The milestones follow the source's supporting statements in order. They establish that the Hilbert–Schmidt sum is independent of the orthonormal basis and defines a norm on its domain; that the operator norm is bounded by this norm and the Hilbert–Schmidt class is stable under multiplication by bounded operators; the bracket identity $\|[u,v]\|_{\mathrm{HS}}=\|[u,v]\|_{\mathrm{op}}=\|u\|\|v\|$; the two bracket composition identities; Proposition A.1, the unique nonsymmetric least-change update for $\|R_1PR_2\|_{\mathrm{HS}}$; and its instance $R_2=I$, Broyden's update (A.5). The goal adds self-adjointness and a single two-sided weight.

The Annex then draws consequences of the goal, which are further milestones: the instance $R=I$ is the psb (Powell symmetric Broyden) update; Proposition A.3 states that for nonzero $y,s$ a self-adjoint positive operator ($\langle Bu,u\rangle>0$ for $u\ne0$) with $Bs=y$ exists if and only if $y=C^*Cs$ for a bijective $C$, if and only if $\langle y,s\rangle>0$; with $R=C^{-1}$ the weight becomes $c=y$ and (A.7) becomes the dfp (Davidon–Fletcher–Powell) update (A.8); and (A.9) is a product form of the dfp update from which its positivity follows when $B$ is self-adjoint positive and $\langle y,s\rangle>0$.

Significance

The theorem gives a precise optimization property to a rank-two symmetric secant formula. It identifies the operator selected by the weighted least-change criterion and guarantees there is no other feasible minimizer with the same value. Taking the weight to be the identity yields the psb update, and taking $R=C^{-1}$ with $C^*Cs=y$ yields the dfp update, so two of the classical symmetric secant formulas are least-change updates for different weights. Proposition A.1 similarly characterizes the rank-one update that becomes Broyden's formula when its right weight is the identity. These consequences explain why the familiar formulas arise from a common variational question, as the Annex states.

The paper supplies a mathematical proof. The remaining formalization work is to represent the Hilbert–Schmidt class, its norm and ideal property, the weighted objectives, and the exact minimization claims in Lean, then prove those claims. Mathlib supplies Hilbert spaces, Hilbert bases, bounded linear maps, adjoints, and the rank-one operator corresponding to the paper's bracket. The statements drafted for this mission compile, but they carry sorry and have no machine-checked proof from this mission yet. A completed development would leave reusable Hilbert–Schmidt and rank-one operator results beyond this quasi-Newton application.

Difficulty

The secant equation alone fixes an operator on only one vector. Even in two dimensions, a rank-one perturbation can satisfy that equation while failing to preserve self-adjointness. Requiring self-adjointness leaves many candidates, and minimizing the two-sided weighted Hilbert–Schmidt norm must distinguish exactly one of them. In infinite-dimensional spaces the norm also has a domain: some bounded operators have an infinite square sum. A formulation that silently assigns a finite default value to a nonsummable operator could turn the least-change claim into a different assertion. These are the mathematical and formal obstacles the milestone list exposes.

Formalization scope

Lean uses an arbitrary complete real inner-product space, with no finite-dimensional or separability assumption, and an arbitrary HilbertBasis index type. Each theorem takes a basis parameter; the basis-independence milestone states why this represents the paper's basis-free norm. The reusable definitions for the bracket and the Hilbert–Schmidt square sum are separate from the paper-specific feasible sets. bracket u v abbreviates Mathlib's rankOne ℝ u v, with $v$ paired with the input. A bijective bounded operator is represented by a continuous linear equivalence $R:\mathcal H\simeq\mathcal H$; the bounded inverse theorem makes this equivalent to the paper's bijective member of $L(\mathcal H)$. The definition of $c$ applies the adjoint of $R^{-1}$ to $R^{-1}s$.

Lean's real tsum has a default value when the family is not summable, so the Hilbert–Schmidt norm is used as a norm only for operators satisfying the explicit summability predicate. Both $\Pi$ and $\Pi_S$ include that predicate. The ideal-property milestone covers the weighted operators in the two objectives. The hypothesis $s\ne0$ is exactly the proposition's condition; it entails $\langle c,s\rangle=\|R^{-1}s\|^2>0$, so no extra nonzero-denominator hypothesis is imposed. The statement spells out “unique solution” as feasibility, minimality over every feasible perturbation, and equality of every feasible minimizer with $P_c$. The paper prints “problem (A.5)” in Proposition A.2, but (A.5) labels Broyden's displayed formula; its preceding paragraph defines the relevant symmetric minimization as (A.6). This mission formalizes (A.6).

In Proposition A.3 and (A.9), "positive" is the paper's strict notion $\langle Bu,u\rangle>0$ for $u\ne0$, not the non-strict positivity of Mathlib. The identity (A.9) is stated for self-adjoint $B$ and $\langle y,s\rangle\ne0$, the setting of the Annex's symmetric problem; the paper's sentence before the psb formula repeats the "(A.5)" misprint and is read as (A.6) in the same way.

The definition layer, basis independence, operator-ideal property, bracket results, both least-change propositions, and the Broyden, psb, dfp and positivity statements are welcome proof targets. The scaling results of §4.1 are outside this mission.

Selected references

• Jean Charles Gilbert and Claude Lemaréchal, Some numerical experiments with variable-storage quasi-Newton algorithms, IIASA Working Paper WP-88-121, August 1988, §2.1 and Annex, printed pp. 3 and 26–30. Working paper PDF.
• Jean Charles Gilbert and Claude Lemaréchal, Some numerical experiments with variable-storage quasi-Newton algorithms, Mathematical Programming 45 (1989), 407–435. DOI 10.1007/BF01589113. Cited for publication history; all statement indices above follow the working paper.

Motivation

Modular composition asks, given univariate polynomials $f, g, h$ over a ring, for $f(g(X)) \bmod h(X)$. It is the bottleneck step in the classical algorithms for factoring univariate polynomials over finite fields (Cantor–Zassenhaus, von zur Gathen–Shoup, Kaltofen–Shoup), for irreducibility testing and for computing minimal polynomials. Brent and Kung (1978) gave an algorithm using $O(n^{(\omega+1)/2})$ operations for degree $n$, and for three decades no algorithm with a near-linear operation count was known in general.

Kedlaya and Umans (Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X) obtained near-linear modular composition over finite fields, and with it asymptotically faster algorithms for factoring polynomials over finite fields. Their route has two halves: a reduction of modular composition to multivariate multipoint evaluation (Section 3), and new fast algorithms for the latter (Sections 4 and 6). This mission formalizes the correctness of the first half, Theorem 3.1. The paper notes that Shoup and Smolensky used essentially the same transformation in an unpublished 1992 manuscript.

Setting

Throughout, $R$ is an arbitrary commutative ring. Variables are indexed from $0$.

MULTIVARIATE MULTIPOINT EVALUATION (Problem 2.1): given $f \in R[X_0, \dots, X_{m-1}]$ with individual degrees at most $d-1$ and points $\alpha_0, \dots, \alpha_{N-1} \in R^m$, output $f(\alpha_0), \dots, f(\alpha_{N-1})$.

MODULAR COMPOSITION (Problem 2.2): given $f \in R[X_0, \dots, X_{m-1}]$ with individual degrees at most $d-1$, and $g_0, \dots, g_{m-1}, h \in R[X]$ of degree at most $N-1$ with the leading coefficient of $h$ a unit, output $f(g_0(X), \dots, g_{m-1}(X)) \bmod h(X)$, the unique $r$ with $\deg r < \deg h$ and $h \mid f(g_0, \dots, g_{m-1}) - r$.

The inverse Kronecker map (Definition 2.3) $\psi_{h,\ell} : R[X_0, \dots, X_{m-1}] \to R[Y_{0,0}, \dots, Y_{m-1,\ell-1}]$ is the $R$-linear map that sends the monomial $\prod_i X_i^{e_i}$ to $\prod_i \prod_{j<\ell} Y_{i,j}^{a_{i,j}}$, where $e_i = \sum_{j \ge 0} a_{i,j} h^j$ is the base-$h$ expansion. It trades individual degree for number of variables: every individual degree of $\psi_{h,\ell}(f)$ is below $h$.

The algorithm of Theorem 3.1 takes $2 \le d_0 < d$, sets $\ell = \lceil \log_{d_0} d \rceil$ and $N' = N m \ell d_0$, receives points $\beta_0, \dots, \beta_{N'-1} \in R$ whose differences are units, and

1. computes $f' = \psi_{d_0,\ell}(f)$;
2. computes $g_{i,j} = g_i^{d_0^{\,j}} \bmod h$ for all $i$ and $j < \ell$;
3. computes $\alpha_{i,j,k} = g_{i,j}(\beta_k)$;
4. computes $f'(\alpha_{0,0,k}, \dots, \alpha_{m-1,\ell-1,k})$ for $k < N'$ (one multivariate multipoint evaluation);
5. interpolates these $N'$ values at the nodes $\beta_k$;
6. outputs the result modulo $h$.

Formalization targets

Goal: Theorem 3.1, correctness

$$\mathrm{algorithm}(d_0, d, f, g, h, \beta) \;=\; f\bigl(g_0(X), \dots, g_{m-1}(X)\bigr) \bmod h(X),$$

for all $m, N \ge 1$, $2 \le d_0 < d$, $f$ with individual degrees $\le d-1$, $g_i, h$ of degree $\le N-1$ with $\mathrm{lc}(h)$ a unit, and $\beta_0, \dots, \beta_{N'-1}$ distinct with unit differences. The right-hand side is stated through the characterization of the remainder (divisibility by $h$ and degree below $\deg h$).

Milestones (in the order the proof uses them)

• Definition 2.3, remark: if every individual degree of $f$ is at most $h^\ell - 1$, then $\psi_{h,\ell}(f)\bigl(X_0^{h^0}, \dots, X_{m-1}^{h^{\ell-1}}\bigr) = f$.
• Definition 2.3, remark: $\psi_{h,\ell}$ is injective on such polynomials (not used by the goal).
• Proof of Theorem 3.1: $f'(g_{0,0}, \dots, g_{m-1,\ell-1}) \equiv f(g_0, \dots, g_{m-1}) \pmod{h}$.
• Proof of Theorem 3.1, Step 5: $\deg f'(g_{0,0}(X), \dots, g_{m-1,\ell-1}(X)) < N'$.

A supporting theorem states that the interpolation formula over a commutative ring (Figure 1) recovers every polynomial of degree $< n$ from its values at $n$ nodes with unit differences.

Significance

Theorem 3.1 says that modular composition is no harder than one multivariate multipoint evaluation with $m\ell$ variables, individual degrees below $d_0$, and $N'$ points, up to quasi-linear univariate work. Combined with the paper's fast multipoint evaluation algorithms this gives modular composition over $\mathbb F_q$ in $n^{1+o(1)}\log^{1+o(1)} q$ bit operations, and from there the paper's improved bounds for polynomial factorization, irreducibility testing, minimal polynomials and modular power projection (Sections 7–8). The converse reduction (Theorem 3.3) shows the two problems are essentially equivalent.

The paper's proof of correctness is a short paragraph; the operation counts are the paper's main concern. This mission makes the correctness exact: the algorithm is defined step for step, and its output is proved equal to the specification. As far as the platform's corpus shows, neither the inverse Kronecker map nor this reduction has a machine-checked statement; the running-time half is not part of this mission.

Difficulty

The obvious argument substitutes $g_i^{d_0^j}$ for $Y_{i,j}$ and invokes the inverse Kronecker identity. Two points keep this from being immediate. First, $\psi_{h,\ell}$ is linear but not multiplicative, and it discards base-$h$ digits beyond position $\ell-1$; the identity holds only for individual degrees at most $h^\ell - 1$, which here requires $d \le d_0^{\lceil \log_{d_0} d\rceil}$. Second, the algorithm never sees $f'(g_{0,0}, \dots)$ itself, only its values at $N'$ points: interpolation recovers it only if its degree is below $N'$, which is why Step 2 reduces modulo $h$ before substituting, and interpolation over a ring (not a field) needs the unit-difference hypothesis throughout. Mathlib's Lagrange interpolation is stated over fields, so the ring version must be handled directly.

Formalization scope

• $R$ is any commutative ring (CommRing R); there is no field or nontriviality assumption.
• Variables are Fin m; the new variables $Y_{i,j}$ are Fin m × Fin ℓ; points are Fin N'.
• Individual degrees are MvPolynomial.degreeOf; "degree at most $N-1$" is natDegree ≤ N - 1.
• $\ell$ is Nat.clog d₀ d and $N' = N m \ell d_0$; $\ell$ is not a free parameter.
• "mod $h$" for $h$ with unit leading coefficient is the remainder on division by the monic associate $h \cdot \mathrm{lc}(h)^{-1}$; interpolation is the Lagrange formula with Ring.inverse of the node differences.
• Step 4 is MvPolynomial.eval, which is exactly the output of Problem 2.1.
• Added hypotheses: $m \ge 1$ and $N \ge 1$ (the paper does not consider $m = 0$, where $N' = 0$, or $N = 0$, where "degree at most $N - 1$" would collapse in natural-number arithmetic).
• In the goal, "$\deg r < \deg h$" is weakened to "$\deg r < \deg h$ or $r = 0$" only to cover the zero ring; in any nontrivial ring the two agree.
• Only correctness is formalized. Operation counts, the $O(\cdot)$ and $\mathrm{poly}\log$ bounds, and the count of invocations are out of scope.

Step 5 is the interpolation formula applied to the $N'$ computed values and nodes alone; it is not defined as the polynomial $f'(g_{0,0}, \dots, g_{m-1,\ell-1})$, and the goal is the six-step output, not the congruence alone, so the statement cannot be closed by unfolding definitions.

Useful infrastructure, reusable beyond this mission: base-$h$ digit manipulation of exponent vectors, Lagrange interpolation over commutative rings with unit node differences, and remainders modulo polynomials with unit leading coefficient. Proofs of any milestone, and of the supporting interpolation theorem, are welcome independently.

Selected references

• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, Dagstuhl Seminar Proceedings 08381, 2008. http://drops.dagstuhl.de/opus/volltexte/2008/1777
• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, SIAM J. Comput. 40(6):1767–1802, 2011. https://doi.org/10.1137/08073408X
• R. P. Brent, H. T. Kung, Fast algorithms for manipulating formal power series, J. ACM 25(4):581–595, 1978. https://doi.org/10.1145/322092.322099
• J. von zur Gathen, J. Gerhard, Modern Computer Algebra, Cambridge University Press, 1999. https://doi.org/10.1017/CBO9781139856065

Motivation

Many objectives in statistics and machine learning are neither smooth nor convex, yet are well behaved in a weaker sense: robust phase retrieval, blind deconvolution, robust PCA and training with piecewise-linear losses all lead to weakly convex functions, functions that become convex after adding a fixed quadratic. For such functions the plain subgradient method $x_{k+1}=x_k-h\,f'(x_k)$ remains the method of choice, and the natural question is how fast it reaches approximate stationarity. Davis and Drusvyatskiy (SIAM J. Optim. 2019) gave the first such rate, measured by the gradient of the Moreau envelope, of order $\widetilde L^2\,4\kappa/\sqrt{N+1}$.

Das Gupta, Van Parys and Ryu (Math. Program. 204 (2024) 567–639) introduced BnB-PEP, a branch-and-bound method for solving nonconvex performance-estimation problems to global optimality, and used it to construct optimal and efficient first-order methods. Their one fully analytical result (§6.3) is a new potential-function analysis of the subgradient method on weakly convex functions with bounded subgradients. It produces an explicit stepsize and a rate that strictly improves on the Davis–Drusvyatskiy bound for all large enough $N$. The certificate was found numerically; the paper then gives a classical proof that can be checked by hand. This mission formalizes that result.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. A function $f:\mathbb R^d\to\mathbb R$ is $\rho$-weakly convex if $f+\frac{\rho}{2}\|\cdot\|^2$ is convex. For such $f$, a vector $g$ is a subgradient of $f$ at $x$, written $g\in\partial f(x)$, when

$$f(y)\ge f(x)+\langle g,y-x\rangle-\frac{\rho}{2}\|y-x\|^2\qquad\forall y\in\mathbb R^d .$$

The class $\mathcal W_{\rho,L}$ consists of the $\rho$-weakly convex $f$ whose subgradients all satisfy $\|g\|\le L$. Since $f\in\mathcal W_{\rho,L}$ exactly when $f/\rho\in\mathcal W_{1,L/\rho}$, the paper sets $\rho=1$ and writes $\widetilde L=L/\rho$; here the normalized bound is written $L$ (Lean: InWeakClass 1 L f, with subgradients IsWeakSubgrad 1 f x g).

For $\hat\rho>1$ the proximal point $\mathrm{prox}_{(1/\hat\rho)f}(x)$ is the unique minimizer of $y\mapsto f(y)+\frac{\hat\rho}{2}\|y-x\|^2$, and the Moreau envelope is the minimum value

$$f_{(1/\hat\rho)}(x)=\min_{y}\Big\{f(y)+\frac{\hat\rho}{2}\|y-x\|^2\Big\}$$

(Lean: SAGA.Convex.IsProxPoint f (1/ρ̂) x y and moreauEnv ρ̂ f x). The envelope is continuously differentiable, and its gradient $\nabla f_{(1/\hat\rho)}(x)=\hat\rho(x-y)$ is a subgradient of $f$ at the prox point $y$. With $\hat\rho=2$, the paper's choice, $\|\nabla f_{(1/2)}(x)\|$ small means that $x$ is near a point $y$ that is nearly stationary for $f$.

The method is $x_{k+1}=x_k-h\,f'(x_k)$ for $k\in[0:N]$, where each $f'(x_k)\in\partial f(x_k)$ is arbitrary. One writes $y_k=\mathrm{prox}_{(1/2)f}(x_k)$, $f'(y_k)=2(x_k-y_k)$, assumes a global minimizer $x_\star$ and the initial condition $f(y_0)-f(x_\star)+\|x_0-y_0\|^2\le R^2$, and sets $\kappa=R/L$.

Formalization targets

Goal: Corollary 1 (p. 625)

For the stepsize $h=\sqrt{4\kappa^2(N+1)+1}\,/\,(2(N+1))$, provided $h\le\frac12$,

$$\frac{1}{N+1}\sum_{i=0}^{N}\|\nabla f_{(1/2)}(x_i)\|^2\ \le\ \frac{L^2\big(2\sqrt{4\kappa^2(N+1)+1}-1\big)}{N+1}.$$

The bound holds for every choice of subgradients along the run.

Theorem 1 (p. 623)

For $h\in(0,\frac12]$, $b_{N+1}=0$, $b_k=4+(1-2h)b_{k+1}$ and $c_k=h^2b_{k+1}$, the potentials $\psi_k=b_k\big(f(y_k)-f(x_\star)+\|x_k-y_k\|^2\big)$ satisfy

$$\|f'(y_k)\|^2+\psi_{k+1}-\psi_k\le c_k\|f'(x_k)\|^2\quad(k\in[0:N]),\qquad \frac{1}{N+1}\sum_{i=0}^{N}\|\nabla f_{(1/2)}(x_i)\|^2\le\frac{1}{N+1}\Big(L^2\sum_{i=0}^{N}c_i+b_0R^2\Big).$$

Milestones

In proof order: the Moreau-envelope facts of §6.3.1; the one-step inequality (32) for an arbitrary point; the telescoping display after (32); the closed form (44) of $b_k$ with nonnegativity; Theorem 1; the closed form (45) of its bound in $h$; the majorant (46) with Bernoulli's upper bound; and the minimizer $h^\star_{\mathrm{ub}}$ of (46) with its value.

Significance

The result. Corollary 1 gives an explicit, non-asymptotic rate for the most basic method of nonsmooth nonconvex optimization, with explicit constants and an explicit stepsize. As $N\to\infty$ the bound is asymptotic to $4\kappa L^2/\sqrt{N+1}$, and the paper shows it is strictly below the earlier bound $L^2\,4\kappa/\sqrt{N+1}$ once $N>(9-64\kappa^2)/(64\kappa^2)$. It also bounds $\min_{i\le N}\|\nabla f_{(1/2)}(x_i)\|^2$. It shows that computer-assisted performance estimation can produce closed-form guarantees beyond the convex, interpolable function classes where PEP is usually applied.

Formalizing it. The result is proved on paper twice (pp. 622–627), but nothing about weakly convex functions, their subdifferential or the Moreau envelope in the nonconvex regime is formalized on the platform, and the convergence analysis has not been machine-checked. A complete development formalizes the potential-function proof and supplies reusable facts about weakly convex functions and the Moreau envelope.

Difficulty

The scalar part of the argument ((44)–(46) and the plug-in) is elementary algebra and one Bernoulli inequality. The analytic weight sits in two places. First, the Moreau envelope of a nonconvex function: showing that the real infimum is attained at the prox point, that the envelope is differentiable with gradient $\hat\rho(x-y)$, and that this gradient is a subgradient of $f$ at $y$ with the weak-convexity modulus $1$ (not the modulus $\hat\rho$ that the prox inequality gives directly). Second, inequality (32): it is not a consequence of convexity, since $f$ is not convex, and it must hold for an arbitrary current point and an arbitrary subgradient, with parameters $b_k,c_k$ fixed in advance. The obvious route through descent of $f$ itself fails: $f(x_k)-f(x_\star)$ need not decrease for nonconvex $f$, which is why the potential uses the envelope at the iterates.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin d), and $f$ is real-valued and defined everywhere. The weak-convexity modulus is normalized to $\rho=1$, and the Lean name L is the paper's $\widetilde L$; the general class $\mathcal W_{\rho,L}$ follows by scaling and is not stated. The subdifferential is the weak-convexity inequality above. For weakly convex $f$ it equals the Clarke, Fréchet and limiting subdifferentials, so it is the paper's abstract $\partial f$ in every admissible instance. The convex subdifferential of $f$ is not used: it can be empty for nonconvex $f$ and would make the statements vacuous. The run is given by sequences x g y : ℕ → E, with g k an arbitrary subgradient at x k for $k\le N$, and y k tied to x k by IsProxPoint f (1/2) for $k\le N+1$. $f'(y_k)$ is not free: it is $2(x_k-y_k)$. The Moreau envelope is a real ⨅; it is finite and attained in this regime, and the first milestone proves this. The parameters $b,c$ of Theorem 1 are pinned by hypotheses, not chosen existentially.

Two hypotheses are made explicit. Corollary 1 is stated "in the setup of Theorem 1", which requires $h\in(0,\frac12]$; for the prescribed stepsize this is $4\kappa^2(N+1)+1\le(N+1)^2$, and it is carried as the hypothesis $h\le\frac12$. It fails for $N=0$ and whenever $\kappa$ is large relative to $N$. Inequality (32) is stated for one arbitrary step, under the nonnegativity of the alternate proof's weights ($h\ge0$, $b_{k+1}\ge0$, $hb_{k+1}\le2$). The minimizer $x_\star$ is assumed, as in the paper; the remark on p. 627 that $\inf f>-\infty$ suffices is not used.

Useful contributions include basic lemmas on weakly convex functions (existence of subgradients, strong convexity of the prox subproblem), differentiability of the Moreau envelope for $\hat\rho>\rho$, the weighted-sum identity behind (32), and Bernoulli's upper bound $(1+a)^r\le 1/(1-ra)$ for $a\in[-1,0]$.

Selected references

• S. Das Gupta, B. P. G. Van Parys, E. K. Ryu, Branch-and-bound performance estimation programming: a unified methodology for constructing optimal optimization methods, Mathematical Programming 204 (2024) 567–639. https://doi.org/10.1007/s10107-023-01973-1
• D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM Journal on Optimization 29(1) (2019) 207–239. https://doi.org/10.1137/18M1178244
• Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Mathematical Programming 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
• A. B. Taylor, J. M. Hendrickx, F. Glineur, Smooth strongly convex interpolation and exact worst-case performance of first-order methods, Mathematical Programming 161 (2017) 307–345. https://doi.org/10.1007/s10107-016-0985-6

Motivation

Nash's existence theorem for finite games is a fixed-point theorem: one writes down a continuous map from the set of mixed strategy profiles to itself whose fixed points are exactly the Nash equilibria, and applies Brouwer's theorem. Nash's own map (Nash 1951) divides by $1+\sum_j \max(0,\cdot)$, and the choice of map matters as soon as the question is computational rather than existential.

Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) introduce the class FIXP of fixed-point search problems whose maps are given by algebraic circuits over $\{+,-,*,/,\max,\min\}$ and rational constants, and show that computing a Nash equilibrium of a 3-player game is FIXP-complete. In Section 4 they ask which gates are really needed. Since the Nash problem is complete, it suffices to find, for every game, a map with the same fixed points and a cheaper circuit. They define a division-free map $G_I$, prove that its fixed points are precisely the Nash equilibria (Lemma 20), show that it is computed by a circuit with gates $\{+,-,*,\max,\min\}$ (Lemma 21), and conclude that FIXP is unchanged if circuits use only $\{+,*,\max\}$ and rational constants (Theorem 22). The same map, defined as a Euclidean projection, appears earlier in Gul, Pearce and Stacchetti (1993).

This mission formalizes the game-theoretic content of that section: the map $G_I$, its well-definedness, and Lemma 20.

Setting

A finite game $I$ has a finite set of players $i$; each player has a finite, nonempty set $S_i$ of pure strategies, and a payoff function $u_i$ assigns a real number to every pure strategy profile. A mixed strategy of player $i$ is a vector $(x_{ij})_{j\in S_i}$ with $x_{ij}\ge0$ and $\sum_{j}x_{ij}=1$; a mixed profile $x$ is one mixed strategy per player, and $\Delta$ denotes the set of mixed profiles (the product of the players' unit simplices). The expected payoff $u_i(x)$ is the expectation of $u_i$ when the players draw their strategies independently according to $x$. For $j\in S_i$, $u_i((i{:}j);x_{-i})$ is player $i$'s expected payoff when $i$ plays $j$ and the others play according to $x$. A Nash equilibrium is a mixed profile $x$ such that no player can raise $u_i(x)$ by switching unilaterally to another mixed strategy.

For a vector $x$ indexed by pairs $(i,j)$, let $v(x)_{ij}=u_i((i{:}j);x_{-i})$ and $h(x)=x+v(x)$. For each player $i$ define the function of a real variable

$$f_{i,x}(t)=\sum_{j\in S_i}\max\bigl(h_{ij}(x)-t,\,0\bigr).$$

It is continuous, nonincreasing, strictly decreasing below $\max_j h_{ij}(x)$ and zero above it, so there is a unique threshold $t_i$ with $f_{i,x}(t_i)=1$. The division-free map is

$$G_I(x)_{ij}=\max\bigl(h_{ij}(x)-t_i,\,0\bigr).$$

In the Lean development, $v(x)_{ij}$ is DGPNash.NashMap.purePayoff u x i j, $h$ is hVal, $f_{i,x}$ is fSum, $t_i$ is threshold and $G_I$ is G, all in the namespace FixpNash.DivFree.

Formalization targets

Goal: Lemma 20 (p. 47)

For every finite game with nonempty strategy sets and every $x\in\Delta$,

$$G_I(x)=x\iff x\text{ is a Nash equilibrium of }I.$$

Milestones, in the order the proof uses them

1. The threshold is well defined (p. 47): for every real $x$ and every player with $S_i\neq\emptyset$, $f_{i,x}(t)=1$ has exactly one solution, and it is $t_i$.
2. $G_I$ maps into $\Delta$ (p. 47): $\sum_{j\in S_i}G_I(x)_{ij}=1$ for every $i$, so $G_I(x)\in\Delta$.
3. Pure deviations suffice (p. 11): $x$ is a Nash equilibrium iff $x\in\Delta$ and $u_i((i{:}j);x_{-i})\le u_i(x)$ for all $i$ and $j\in S_i$.
4. Fixed points equalize the support (proof of Lemma 20, p. 47): if $x\in\Delta$ and $G_I(x)=x$, then $u_i((i{:}j);x_{-i})=t_i$ when $x_{ij}>0$ and $u_i((i{:}j);x_{-i})\le t_i$ when $x_{ij}=0$.
5. At an equilibrium the threshold is the payoff (proof of Lemma 20, p. 47): if $x$ is a Nash equilibrium then $t_i=u_i(x)$ for every $i$.
6. Closed form of the threshold (proof of Lemma 21, p. 48): if $z_{i1}\ge\dots\ge z_{in_i}$ is $h_i(x)$ sorted in decreasing order, then

$$t_i=\max\Bigl\{\tfrac1l\Bigl(\sum_{j=1}^{l}z_{ij}-1\Bigr):l=1,\dots,n_i\Bigr\}.$$

This last milestone is off the goal's path; it is the formula behind the division-free circuit.

Significance

Lemma 20, with Brouwer's theorem and the continuity of $G_I$, gives an elementary proof of Nash's theorem. With Lemma 21 it shows that the Nash equilibrium problem, and therefore every FIXP problem, is represented by circuits without division; the paper uses this to obtain Theorem 22. The pure-deviation criterion of milestone 3 is the standard test for equilibria and is used throughout equilibrium computation. The closed form of milestone 6 is the threshold of the Euclidean projection onto the simplex, used widely in optimization.

All of these results are proved in the paper. The mission produces machine-checked versions. No platform item states Lemma 20 or the pure-deviation criterion for AGT.IsMixedNash. Related posed items, with other conventions, are credited below rather than reused: the thresholds of the simplex projection in the Condat 2015 series (SimplexProj.Condat.simplex_projection_threshold, threshold_root_bracket, subsequence_mean_le_threshold, stated for the projection on $\mathbb R^N$ with a radius), and the best-response fixed-point characterization in supermodular games (Supermodularity.Games.equilibrium_iff_fixed_point_v2, a different map). The paper also remarks, without proof, that $G_I(x)$ is the point of $\Delta$ closest to $h(x)$. That remark is not a target here.

Difficulty

The map $G_I$ is defined through an implicitly determined threshold. In the formalization the threshold has to be a definition that does not depend on a proof, and every statement about it rests on the existence and uniqueness of the root of $f_{i,x}(t)=1$. This is an intermediate-value argument for a piecewise linear function of a finite sum of $\max$ terms. Its strict monotonicity holds only below $\max_j h_{ij}(x)$, and the argument must use that $S_i$ is nonempty.

The equivalence itself needs the multilinearity of the expected payoff: $u_i(x)=\sum_j x_{ij}\,u_i((i{:}j);x_{-i})$ and, more generally, the payoff of a deviation to a mixed strategy $y_i$ is $\sum_j y_{ij}\,u_i((i{:}j);x_{-i})$. In the agt_games representation the expected payoff is a sum over all pure profiles of products of probabilities, so this identity must be extracted from the product structure rather than read off.

Formalization scope

The game uses the published agt_games vocabulary: players form a finite type ι with decidable equality, the strategies of player i a finite type S i, payoffs are real (the paper's are rational, so this is a generalization), mixed profiles are real weight functions satisfying AGT.IsMixedProfile, and Nash equilibrium is AGT.IsMixedNash (no profitable deviation to any lottery). The pure-strategy payoff $u_i((i{:}j);x_{-i})$ is the published DGPNash.NashMap.purePayoff.

The following readings are explicit in the Lean and implicit on the page:

• every strategy set is nonempty (∀ i, Nonempty (S i)). The paper assumes this tacitly; without it $\Delta$ is empty and $t_i$ does not exist;
• the threshold is defined as $t_i=\inf\{t: f_{i,x}(t)\le1\}$. Milestone 1 proves that this is the paper's "unique value of $t$ where $f_{i,x}(t_i)=1$". A formalization in which $t_i$ is a free parameter, or is set to $u_i(x)$, would make Lemma 20 nearly definitional. That is ruled out: $G_I$ is defined from the game alone, and $t_i$ is the root of $f_{i,x}(t)=1$;
• $h$, $f_{i,x}$, $t_i$ and $G_I$ are given by the same formulas for every real vector $x$. Milestones 1, 2 and 6 hold in that generality, while the goal and milestones 4–5 are stated on $\Delta$, as on the page;
• "fixed point of $G_I$" means a point $x\in\Delta$ with $G_I(x)=x$;
• "it is sufficient to check switches to pure strategies only" becomes an equivalence between AGT.IsMixedNash and the pure-deviation inequalities for a mixed profile;
• in milestone 6, the sorted order is a bijection $e$ from $\{0,\dots,n\}$ onto $S_i$ along which $h_{i,e(l)}(x)$ is nonincreasing, so $n_i=n+1$ and the paper's index $l$ is $l+1$.

Contributions welcome: proofs of any milestone. The multilinearity of AGT.expectedPayoff in one player's strategy, and the existence and uniqueness of the threshold of a finite sum of hinge functions, are reusable beyond this mission.

Selected references

• K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points, SIAM J. Comput. 39(6) (2010) 2531–2597; author manuscript, Section 4, pp. 47–48. https://doi.org/10.1137/080720826
• J. Nash, Non-cooperative games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529
• F. Gul, D. Pearce and E. Stacchetti, A bound on the proportion of pure strategy equilibria in generic games, Mathematics of Operations Research 18(3) (1993) 548–552. https://doi.org/10.1287/moor.18.3.548
• L. Condat, Fast projection onto the simplex and the ℓ1 ball, Mathematical Programming 158 (2016) 575–585. https://doi.org/10.1007/s10107-015-0946-6