Completed

Graph Theory Number Theory·Captain: xiangyazi24

Proofs from THE BOOKTextbook

Proofs from THE BOOK: verified results and open formalization tasks

This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's Proofs from THE BOOK. It combines results imported from the existing proof_in_the_book repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.

What is already verified

The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.

The imported source snapshot is 873d52e0c88cd351f594221e70c3c5b3559777a9. Imported results use Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.

The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.

Sixth-edition contribution targets

New milestones explicitly marked 6th ed. cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.

Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.

The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.

Chapter numbering and statement scope

Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.

Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.

How to contribute

Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.

Source repository: https://github.com/xiangyazi24/proof_in_the_book

Book: Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8

209 thms11 active users

Algebra Analysis Functional Analysis+3·Captain: Lucas

Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem

1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
1962 — Radó: the busy beaver function outgrows every computable function.
1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$ .
1978 — Apéry: $\zeta(3)$ is irrational.
1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$ .
2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$ .

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$ , and $f$ is irreducible over $\mathbb{Z}$ ; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$ , and let

\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.

The Bateman–Horn constant is the (conditionally convergent) Euler product

C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$ ; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$ ; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$ .

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$ , $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$ , Kakeya over $\mathbb{F}_q$ , Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ( $\zeta(5)$ , all odd zeta values, Zudilin's theorem, $e+\pi$ , $e\pi$ , $\gamma$ , Catalan's constant), order theory (the $1/3$ – $2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$ , and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$ , $\deg f = 2$ : sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$ .
The Bateman–Horn constant is the limit of the ordered partial products over $p<N$ , not an unordered infinite product.
Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$ .
Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$ .
Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$ , and probabilities are quotients of set cardinalities in $\mathbb{Q}$ .
The busy beaver model is an explicit $n$ -state, $2$ -symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$ .
Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. " $e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$ ?", is replaced by Radó's growth theorem rather than guessed at.
Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$ , Bull. London Math. Soc. 17 (1985), 305–317. DOI
K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

81 thms8 active usersReviewed

Completed

Complexity Theory Graph Theory Operations Research+1·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity II: Unit-Time Jobs on Two Uniform Machines with Unit Resources Are Strongly NP-hardResearch Paper

Motivation

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\,|\,\beta\,|\,\gamma$ of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field $res\lambda\sigma\rho$ . They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.

This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$ . Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine $M_i$ has a speed $q_i>0$ , and every job has unit execution requirement $p_j=1$ , so it takes time $1/q_i$ on $M_i$ . Identical machines ( $P$ ) are the case $q_i=1$ ; uniform machines ( $Q$ ) allow arbitrary speeds.

There are $l$ resources $R_1,\dots,R_l$ . Resource $R_h$ has a positive integer size $s_h$ , the amount available at any time. Job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. A schedule assigns each job a machine $\mu(j)$ and a start time $S_j\ge 0$ . Its completion time is $C_j=S_j+1/q_{\mu(j)}$ , and it is being executed at every time $t$ with $S_j\le t<C_j$ . A schedule is feasible when:

jobs on the same machine do not overlap in time;
at every time $t$ , the set $S_t$ of jobs being executed satisfies

\sum_{j\in S_t} r_{hj}\le s_h\qquad(h=1,\dots,l).

The makespan is $C_{\max}=\max_j C_j$ .

The resource type $res{\cdot}11$ means three things: the number $l$ of resources is part of the input, every size is $s_h=1$ , and every requirement satisfies $r_{hj}\le1$ . A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. $Pm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ and $Qm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold $y$ , whether a feasible schedule with $C_{\max}\le y$ exists.

The source problems are two graph problems on a graph $G=(V,E)$ with $|V|=3t$ :

PARTITION INTO TRIANGLES: can $V$ be partitioned into $t$ triples of pairwise adjacent vertices?
PARTITION INTO PATHS OF LENGTH 2: can $V$ be partitioned into $t$ triples, each with at most one nonadjacent pair, that is, each spanning a path of length 2?

Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).

The construction of p. 15 introduces one job per vertex and one unit resource $R_{\{j,k\}}$ per nonadjacent pair $\{j,k\}$ , required by $J_j$ and $J_k$ only.

Formalization targets

Goal: Theorem 3

Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}\ \text{is NP-hard in the strong sense.}

Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of $Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard. The two speeds are arbitrary positive integers.

Milestones

The construction's key property (p. 15). In the constructed instance, two distinct jobs can be executed simultaneously if and only if their vertices are adjacent.
The triangle equivalence (proof of Theorem 2). $G$ has a partition into triangles if and only if the constructed instance on three identical machines has a feasible schedule with $C_{\max}\le t$ .
Theorem 2. $P3\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard in the strong sense, given the NP-hardness of PARTITION INTO TRIANGLES.
The paths equivalence (proof of Theorem 3). $G$ has a partition into paths of length 2 if and only if the constructed instance on two uniform machines with speeds $q_1=2$ , $q_2=1$ has a feasible schedule with $C_{\max}\le t$ .

Significance

The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for $\sum C_j$ and $L_{\max}$ from these instances.

Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.

Difficulty

The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time $\tfrac12$ and $1$ , so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.

The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.

Formalization scope

Time and schedules. Start times are nonnegative reals, execution intervals are half-open $[S_j,C_j)$ , and the resource constraints are imposed at every real time. Schedules are nonpreemptive.
Indices. Jobs, machines and resources are 0-based (Fin n, Fin m, Fin l), so $q_1,q_2$ are q 0, q 1.
Decision versions. "NP-hard" refers to the decision version with a threshold $y$ . Thresholds are natural numbers and the $Q2$ speeds are positive integers. This restricted problem is a subproblem of the one with rational data, so its hardness is the stronger statement.
Encodings and strong NP-hardness. Instances are strings over a two-letter alphabet with every number in unary. Graphs are $t$ in unary followed by the $3t\times 3t$ adjacency matrix, so $|V|=3t$ is part of the instance. Languages contain only codes of yes-instances. Strong NP-hardness is NP-hardness of the unary code language. With unary numbers, $\mathrm{Max}(I)\le\mathrm{Length}(I)$ , so this is equivalent to Garey and Johnson's definition. The complexity layer is the published module CookPvsNP_defs.
Cited hypothesis. Each hardness theorem takes as its only hypothesis the NP-hardness of its source problem, which the paper cites from Garey and Johnson rather than proves. The hypothesis is a true statement about a nonempty, non-universal language. The statements are not weakened to a reduction between languages, and they assume nothing about P versus NP.
Source problems. The paper's phrase "three vertices, at most two of which are nonadjacent" is read as "at most one nonadjacent pair", which is Garey and Johnson's GT13. Reading it as "at most two nonadjacent pairs" would admit triples with a single edge and change the problem. PARTITION INTO PATHS OF LENGTH 2 reuses the published definition CubicP3Partition.P3Factor, a spanning non-induced $P_3$ -factor.
Construction. Resources are indexed by the nonadjacent pairs $j<k$ in lexicographic order, one per unordered pair and none for a pair $\{j,j\}$ . A diagonal resource would make every job infeasible.
Not trivial. A model that checks resources only at integer times, or only at start times, would make the paths equivalence false. A hypothesis on the target problem would make the goal circular. The definitions rule out both.

Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.

Selected references

J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979, ISBN 0-7167-1045-5.
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 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

41 thms7 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Convexity and Steinitz's Exchange Property III: Fenchel-Type Min-Max Duality with Primal and Dual Integrality for M-Concave and M-Convex FunctionsResearch Paper

Motivation

Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.

Timeline:

1970: Edmonds proves the polymatroid intersection theorem.
1982: Frank proves the discrete separation theorem for submodular/supermodular set functions, with integrality.
1984: Fujishige proves a Fenchel-type min-max theorem for submodular functions.
1976–1981: Iri and Tomizawa characterize optimality for independent assignment by potentials; Frank proves the weight splitting theorem for weighted matroid intersection (1981).
Early 1990s: Dress and Wenzel introduce valuated matroids.
1995–1996: Murota proves the valuated matroid intersection theorem (SIAM J. Discrete Math. 9, 1996) and the M-concave intersection theorem (Bonn report, 1995), and in the present paper the Fenchel-type duality (Theorem 6.4).
Later: the result becomes the central duality theorem of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM, 2003).

Setting

Let $V$ be a finite nonempty set. For $u\in V$ , $\chi_u\in\mathbb Z^V$ is its characteristic vector; for $x\in\mathbb R^V$ , $\operatorname{supp}^{\pm}(x)$ are the sets of coordinates where $x$ is positive or negative, $x(X)=\sum_{v\in X}x(v)$ , and $\langle p,x\rangle=\sum_v p(v)x(v)$ .

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v\in B$ . These are exactly the integer points of integral base polytopes of submodular systems. $\overline B$ is the convex hull of $B$ .

A function $\omega:B\to\mathbb R$ has the exchange property (EXC), and is called M-concave, if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and

\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v).

A function $\zeta$ is M-convex when $-\zeta$ is M-concave.

For $\omega:B_1\to\mathbb R$ and $\zeta:B_2\to\mathbb R$ the concave conjugate and convex conjugate are

\omega^\circ(p)=\min_{x\in B_1}\big(\langle p,x\rangle-\omega(x)\big),\qquad \zeta^\bullet(p)=\max_{x\in B_2}\big(\langle p,x\rangle-\zeta(x)\big),

and the concave closure and convex closure are $\hat\omega(b)=\inf_p(\langle p,b\rangle-\omega^\circ(p))$ and $\check\zeta(b)=\sup_p(\langle p,b\rangle-\zeta^\bullet(p))$ ; they are finite exactly on $\overline{B_1}$ and $\overline{B_2}$ .

The primal problem maximizes $\omega(x)-\zeta(x)$ over $x\in B_1\cap B_2$ ; the relaxed primal problem maximizes $\hat\omega(b)-\check\zeta(b)$ over $b\in\overline{B_1}\cap\overline{B_2}$ ; the dual problem minimizes $\zeta^\bullet(p)-\omega^\circ(p)$ over $p\in\mathbb R^V$ . A maximum over an empty family is $-\infty$ .

Formalization targets

Goal: Theorem 6.4

If $\omega$ and $-\zeta$ satisfy (EXC), then

\max_{x\in B_1\cap B_2}\big(\omega(x)-\zeta(x)\big)=\max_{b\in\overline{B_1}\cap\overline{B_2}}\big(\hat\omega(b)-\check\zeta(b)\big)=\inf_{p\in\mathbb R^V}\big(\zeta^\bullet(p)-\omega^\circ(p)\big),

with (P1) a finite dual infimum forces $B_1\cap B_2\neq\emptyset$ , and (P2) if $B_1\cap B_2\neq\emptyset$ all values are finite and equal and the infimum is attained. If $\omega,\zeta$ are integer-valued, the infimum may be taken over $p\in\mathbb Z^V$ and is attained there when finite.

Milestones

Lemma 6.3 (weak duality): for arbitrary $\omega,\zeta$ on finite nonempty sets, primal $\le$ relaxed $=$ dual (the Fenchel identity (6.5)).
Lemma 6.1: $(-f)^\circ(p)=-f^\bullet(-p)$ and $(-f)^\wedge=-\check f$ on $\overline B$ .
Lemma 4.5: an M-concave $\omega$ satisfies $\hat\omega=\omega$ on $B$ .
Theorem 2.1: (B1) is equivalent to being the integer points of an integral submodular (or supermodular) base polytope, with the describing functions $\max_{x\in B}x(X)$ and $\min_{x\in B}x(X)$ .
Theorem 6.5 (Frank's discrete separation theorem, cited in the paper).
Lemma 6.7: four equivalent forms of boundedness of the dual problem.
Theorem 6.6 (the M-concave intersection theorem, cited in the paper): optimality of $x^*$ for $\omega_1+\omega_2$ is equivalent to a potential $p^*$ with $x^*$ maximizing both $\omega_1[-p^*]$ and $\omega_2[p^*]$ , integral when the data are.

Significance

The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.

All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.

Difficulty

Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope $\overline{B_1}\cap\overline{B_2}$ must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of $\overline{B_1}\cap\overline{B_2}$ (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that $p$ can be taken integral, is again specific to (EXC) and fails for general concave extensions.

Formalization scope

Lean conventions, all in namespace SteinitzExchange.Duality:

$V$ is a type with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).
A function on $B$ is a total (V → ℤ) → ℝ used only at points of $B$ . M-convexity of $\zeta$ is (EXC) for fun x => -ζ x; $\omega$ lives on $B_1$ and $\zeta$ on $B_2$ , which are distinct sets in general.
Conjugates are real-valued min/max over the finite set. The closures are real ⨅/⨆ over $p\in\mathbb R^V$ and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of $\mp\infty$ , which no statement uses.
The three optimal values are in EReal, as suprema and infima of coerced reals, so no $\infty-\infty$ occurs. EReal's supremum of the empty family is $-\infty$ , the paper's convention. The dual infimum is never a real ⨅ (which would return $0$ when unbounded and make (P1) meaningless).
Every "max" of the page includes attainment: (P2) asserts points $x$ , $b$ , $p$ at which the three values are achieved; the integral dual infimum is attained when it is not $-\infty$ .
"Integer-valued" means $\omega(x)\in\mathbb Z$ on $B_1$ and $\zeta(x)\in\mathbb Z$ on $B_2$ ; integral potentials and separating vectors are V → ℤ.
Theorem 2.1's " $\forall X\subset V$ " is read as all $X\subseteq V$ .

Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from $\zeta^\circ$ instead of $\zeta^\bullet$ , a single base set for both functions, and a relaxed maximum taken over all of $\mathbb R^V$ instead of $\overline{B_1}\cap\overline{B_2}$ .

Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.

Selected references

K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
K. Murota, Valuated matroid intersection I: optimality criteria, SIAM J. Discrete Math. 9 (1996) 545–561.
K. Murota, Submodular flow problem with a nonseparable cost function, Report 95843-OR, Forschungsinstitut für Diskrete Mathematik, Universität Bonn, 1995 (source of Theorem 6.6).
A. Frank, An algorithm for submodular functions on graphs, Annals of Discrete Mathematics 16 (1982) 97–120 (source of Theorem 6.5).
A. Frank, A weighted matroid intersection algorithm, J. Algorithms 2 (1981) 328–336.
J. Edmonds, Submodular functions, matroids and certain polyhedra, in: Combinatorial Structures and Their Applications, Gordon and Breach, New York, 1970, 69–87.
S. Fujishige, Theory of submodular programs: a Fenchel-type min-max theorem and subgradients of submodular functions, Mathematical Programming 29 (1984) 142–155.
M. Iri and N. Tomizawa, An algorithm for finding an optimal "independent assignment", J. Oper. Res. Soc. Japan 19 (1976) 32–57.
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

18 thms7 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Convexity and Steinitz's Exchange Property I: The Extension Theorem — M-Concavity Is Concave Extendability with Integral Base Polytope MaximizersResearch Paper

Motivation

Linear optimization over the bases of a matroid, over the integer points of a polymatroid, or over the flows of a network is well understood: the greedy algorithm is exact, the feasible sets are the integer points of polytopes described by submodular functions, and min-max theorems of Edmonds and Frank hold with integrality. Nonlinear objectives on the same sets are much less uniform. Valuated matroids (Dress and Wenzel, 1990; see Murota 2003) showed that a quantitative form of the Steinitz exchange axiom is exactly what keeps the greedy algorithm exact for a nonlinear weight. Kazuo Murota's paper Convexity and Steinitz's Exchange Property (Adv. Math. 124 (1996) 272–311) extends this exchange axiom from matroid bases to the integer points of arbitrary integral base polytopes, names the resulting functions M-concave, and proves that they are the discrete counterpart of concave functions. The paper is the starting point of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003), which is now used in auction theory (gross-substitutes valuations are M♮-concave), inventory and resource allocation, and combinatorial optimization.

This mission covers the first of the paper's three characterizations of M-concavity: the Extension Theorem (Theorem 4.6).

Setting

Let $V$ be a finite nonempty set. For $u\in V$ , $\chi_u\in\mathbb Z^V$ is the characteristic vector of $u$ . For $x\in\mathbb R^V$ , $\operatorname{supp}^+(x)=\{v\mid x(v)>0\}$ , $\operatorname{supp}^-(x)=\{v\mid x(v)<0\}$ , $\|x\|=\sum_v|x(v)|$ , and $\langle p,x\rangle=\sum_v p(v)x(v)$ .

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v\in B$ (axiom (B1)). Examples are the incidence vectors of the bases of a matroid. Its convex hull $\overline B$ is an integral base polytope; in general, an integral base polytope is the convex hull of some finite integral base set.

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC), and is called M-concave, if for all $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v\in B$ , $y+\chi_u-\chi_v\in B$ and

\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v).

The local exchange property (EXC $_{\mathrm{loc}}$ ) asks only, for $x,y\in B$ with $\|x-y\|=4$ , for some $u\in\operatorname{supp}^+(x-y)$ and some $v\in\operatorname{supp}^-(x-y)$ with the same conclusion.

For $p\in\mathbb R^V$ , $\omega[p](x)=\omega(x)+\langle p,x\rangle$ , and $\operatorname{argmax}(\omega)=\{x\in B\mid\omega(x)\ge\omega(y)\ \forall y\in B\}$ . For any $g:B\to\mathbb R$ , the concave conjugate is $g^\circ(p)=\min_{x\in B}(\langle p,x\rangle-g(x))$ and the concave closure is $\hat g(b)=\inf_{p\in\mathbb R^V}(\langle p,b\rangle-g^\circ(p))$ , a concave function that is finite exactly on $\overline B$ . A function $\bar\omega:\overline B\to\mathbb R$ extends $\omega$ if $\bar\omega=\omega$ on $B$ .

Formalization targets

Goal: the Extension Theorem (Theorem 4.6)

For a finite integral base set $B$ and $\omega:B\to\mathbb R$ ,

\omega\ \text{satisfies (EXC)}\iff\exists\,\bar\omega:\overline B\to\mathbb R\ \text{concave},\ \bar\omega|_B=\omega,\ \forall p:\ \operatorname{argmax}_{\overline B}(\bar\omega[p])\ \text{is an integral base polytope}.

Milestones

Lemma 3.2 (p. 282): under (EXC $_{\mathrm{loc}}$ ), for $y=x-\chi_{u_0}-\chi_{u_1}+\chi_{v_0}+\chi_{v_1}\in B$ , $\omega_p(y)-\omega_p(x)\le\max(\pi_{00}+\pi_{11},\pi_{01}+\pi_{10})$ with $\pi_{ij}=\omega_p(x-\chi_{u_i}+\chi_{v_j})-\omega_p(x)$ ( $-\infty$ off $B$ ).
Theorem 3.1 (p. 282): (EXC) $\iff$ (EXC $_{\mathrm{loc}}$ ).
Theorem 2.2 (p. 280): (EXC) for $\omega$ implies (EXC) for every $\omega[p]$ .
Lemma 4.3 (p. 285): under (EXC), $\operatorname{argmax}(\omega)$ is an integral base set.
Lemma 4.1 (p. 285): $\hat g\ge g$ on $B$ ; $\max_{\overline B}\hat g=\max_B g$ ; $\operatorname{argmax}(\hat g)=\overline{\operatorname{argmax}(g)}$ .
Lemma 4.2 (p. 285): $(g[p_0])^\circ(p)=g^\circ(p-p_0)$ and $(g[p_0])^\wedge=\hat g+\langle p_0,\cdot\rangle$ on $\overline B$ .
Theorem 4.4 (p. 286): (EXC) $\iff$ $\operatorname{argmax}(\omega[p])$ is an integral base set for every $p$ .
Lemma 4.5 (p. 288): under (EXC), $\hat\omega=\omega$ on $B$ .

Significance

The Extension Theorem identifies a combinatorial axiom with a convex-analytic property: M-concave functions are exactly the restrictions to lattice points of concave functions on the base polytope whose linear perturbations are all maximized on integral base polytopes. It is the reason the M-concave class supports a convex-analysis-style theory at all: local optimality implies global optimality, maximizers of linear perturbations are well behaved, and conjugacy (the paper's Theorems 5.3 and 6.4, separate missions of this series) can be developed. Theorem 3.1 on its own is widely used to verify M-concavity in applications, since it reduces the exchange axiom to pairs at distance four.

All results here were proved in 1996. To our knowledge none of them has a machine-checked proof; Mathlib has matroids on sets but no integral base sets in $\mathbb Z^V$ , no M-concave functions and no concave closure of a function on a finite set. A formal proof of this chain would be a first formal development of discrete convex analysis.

Difficulty

The equivalence of (EXC) with its local version (Theorem 3.1) is not a routine induction on $\|x-y\|$ : the exchange inequality for a far pair does not follow from the inequalities along a path of distance-4 pairs, because the exchange partner $v$ must be chosen consistently with the prescribed $u$ . For the "if" direction of Theorem 4.4, knowing that every maximizer set is an integral base set says nothing directly about the values of $\omega$ at non-maximizing points; turning this global information on maximizers into the local inequality (EXC $_{\mathrm{loc}}$ ) requires a supporting hyperplane of the concave closure at a well-chosen point and the integrality of the intersection of an integral base polytope with a box (a cited result on submodular systems). Theorem 4.6 then needs the concave closure to agree with $\omega$ on $B$ (Lemma 4.5), which fails for general $\omega$ .

Formalization scope

All declarations live in the namespace SteinitzExchange.Extension. The ground set is a type V with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ, and toReal embeds the former into the latter. $B$ is a Finset (V → ℤ). A function $\omega:B\to\mathbb R$ is a total (V → ℤ) → ℝ whose values are only ever read at points required to be in $B$ . $\overline B$ is Mathlib's convexHull ℝ of the image of $B$ . Pinned readings:

Integral base polytope means the convex hull of a finite nonempty set satisfying (B1) (by the paper's Theorem 2.1 this is its meaning), not "a polytope with integer vertices".
The concave closure is a real infimum; it is the paper's value on $\overline B$ and a junk value $0$ off $\overline B$ (the paper's $-\infty$ ), so every statement uses it only on $\overline B$ . $\operatorname{argmax}(\hat g)$ and $\operatorname{argmax}(\bar\omega[p])$ range over $\overline B$ only; the concave conjugate is a minimum over the nonempty finite $B$ .
Lemma 3.2's maximum with $-\infty$ entries is stated as: for one of the two pairings both exchanged points lie in $B$ and the bound holds for that pairing.
Theorem 4.4 and Lemma 4.3 conclude that $\operatorname{argmax}(\omega[p])$ is itself an integral base set. Read literally ("its convex hull is an integral base polytope") the "if" direction of Theorem 4.4 is false: $B=\{(2,0),(1,1),(0,2)\}$ with $\omega=(0,-1,0)$ is a counterexample. The paper's proof, its gloss in Lemma 4.3 and its use on p. 292 all take the integral-base-set reading. Theorem 4.6 needs no such adjustment and is stated as printed.
Theorem 2.2 carries the standing assumption of §2.3 that $\omega$ satisfies (EXC).

Trivializing formalizations are ruled out: the extension $\bar\omega$ must agree with $\omega$ on $B$ and be concave on $\overline B$ , the argmax is over $\overline B$ and not over $\mathbb R^V$ , and an integral base polytope is never empty.

A complete development needs basic facts on integral base sets (the equivalence of (B1) with the simultaneous exchange (B2), $B=\mathbb Z^V\cap\overline B$ , and the paper's cited Theorem 2.1 relating them to submodular functions), the representation (4.3) of the concave closure as a maximum of convex combinations, and supporting hyperplanes of polyhedral concave functions. The layer of integral base sets and M-concave functions is reusable for the two other missions of this series and for any later formalization of discrete convex analysis; contributions of general-purpose lemmas about it are welcome.

Selected references

K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
K. Murota, Discrete Convex Analysis, SIAM Monographs on Discrete Mathematics and Applications, 2003. https://doi.org/10.1137/1.9780898718508

21 thms7 active usersReviewed

Completed

Number Theory·Captain: aarontcao

The Komlos-Sulyok-Szemeredi bound: every finite set of reals has a Sidon subset of size c sqrt nResearch Paper

Call a set of reals a Sidon set when all its pairwise sums are distinct: if $a + b = c + d$ with all four in the set, then $\{a,b\} = \{c,d\}$ .

The goal. There is an absolute constant $c > 0$ such that every finite set $X$ of positive reals contains a Sidon subset $S$ with $|S| \ge c\sqrt{|X|}$ .

This is the lower bound half of Erdos problem 530, which Riddell posed and which asks for the order of the largest guaranteed Sidon subset. That problem is open: it asks whether the guarantee is asymptotically $N^{1/2}$ , and the constant is not known. What is settled is the order, by Komlos, Sulyok, and Szemeredi, Linear problems in combinatorial number theory, Acta Math. Acad. Sci. Hungar. 26 (1975) 113-121, as a case of a general theorem about linear equations. Erdos had previously observed the cube-root lower bound and the matching $(1+o(1))N^{1/2}$ upper bound from $A = \{1, \dots, N\}$ . A second and much shorter proof is in Bailleul and Riblet, arXiv:2605.03181.

The exponent is the whole problem

A one-paragraph argument gives $|S| \ge c|X|^{1/3}$ : take a Sidon subset $S$ of maximum size, and note that every $x$ outside it satisfies $x = c + d - b$ or $x = (c+d)/2$ for elements of $S$ , so $|X| \le 3|S|^3$ .

That cube root is not a weak first attempt, it is the ceiling for any argument that only counts. An arithmetic progression of length $n$ has additive energy of order $n^3$ , so a probabilistic argument cannot see the difference between it and a generic set. Getting from $1/3$ to $1/2$ requires using the structure of the set, and that is what both published proofs do.

The idea both proofs share

Compress, then pigeonhole against a known Sidon set.

An arbitrary finite set of reals has no arithmetic to work with, so first move it into $\mathbb{Z}$ : a finite set spans a finite dimensional $\mathbb{Q}$ -vector space, and a generic rational functional separates its points while preserving every relation $a + b = c + d$ . Then squeeze the resulting integers into an interval of length comparable to their number, keeping a constant fraction of them and keeping the property that a Sidon subset of the image lifts to one of the original. Finally intersect with a translate of the Erdos-Turan Sidon set, which has about $\sqrt{N}$ elements inside $\{0, \dots, N-1\}$ . A set of size $\Theta(n)$ inside $[1,n]$ meets some translate of a Sidon set of size $\sqrt{n}$ in order $\sqrt{n}$ points, and that intersection is Sidon.

The two proofs differ only in the compression step, and the mission carries both.

The two routes

The 1975 route compresses in four lemmas driven by a remainder map: choose a modulus $q$ dividing no difference, dilate so that the remainders are small, and observe that a small remainder map preserves $a + b = c + d$ . Finding the modulus needs a prime counting bound.

The 2026 route replaces all four with one averaging lemma over a real rotation parameter $\theta$ , keeping the elements whose fractional part of $am\theta$ is below $1/2$ , where no carry occurs. No prime counting appears anywhere.

Notes on the formalization

Every item is stated in Mathlib primitives alone, so the mission needs no definition items. The Sidon condition, the Erdos-Turan construction, and the reduction relation of the 1975 route are all written out at each use.

The published 2026 proof finishes with Singer's 1938 covering of $\mathbb{Z}/(q^2+q+1)\mathbb{Z}$ by $q+1$ Sidon sets. Mathlib has no perfect difference sets, so the mission uses averaging over translates instead. It does the same job at the same order and gives a worse constant, which costs nothing because the goal asserts only that some $c > 0$ exists.

Two lemmas of the 1975 paper are deliberately absent. A local formalization of Lemma 2 and Lemma 6 turned out to be false as stated, machine-checked in both cases, so neither is offered here as a milestone. Those are errors in that rendering rather than in the paper, and the 2026 route reaches the goal without either. Lemma 1' is absent for the same practical reason: the 2026 route does not need it.

17 thms7 active usersReviewed

Graph Theory·Captain: Gabewhigham

Conway's 99-graph problemOpen Problem

Motivation

A strongly regular graph with parameters $(n,k,\lambda,\mu)$ is a finite simple graph on $n$ vertices in which every vertex has exactly $k$ neighbours, every pair of adjacent vertices has exactly $\lambda$ common neighbours, and every pair of non-adjacent vertices has exactly $\mu$ common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple $(99,14,1,2)$ is the smallest such case in the family $\lambda = 1$ , $\mu = 2$ , and its existence has been open for more than fifty years. John Horton Conway offered $1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences (Conway, Five $1,000 Problems (Update 2017)).

Timeline of the problem and of what is known about it:

1969/1971 — the parameter set is raised by Norman Biggs in his Southampton lectures (Finite Groups of Automorphisms, LMS Lecture Note Series 6, p. 111).
1973 — Berlekamp, van Lint and Seidel construct a strongly regular graph with parameters $(243,22,1,2)$ as the coset graph of the perfect ternary Golay code, settling one of the five feasible parameter tuples in this family.
1975 — the existence question appears as Problem 7 (attributed to J. J. Seidel) in R. K. Guy's problem list, The Geometry of Metric and Linear Spaces, Springer LNM 490, pp. 237–238; Conway had worked on it by then.
1984 — H. A. Wilbrink, On the $(99,14,1,2)$ strongly regular graph, shows that such a graph cannot be vertex-transitive: no group of automorphisms can act transitively on its 99 vertices.
1988 — Brouwer and Neumaier, A remark on partial linear spaces of girth 5 with an application to strongly regular graphs, Combinatorica 8, 57–61.
2004 — Makhnev and Minakova, On automorphisms of strongly regular graphs with $\lambda=1$ , $\mu=2$ , Discrete Math. Appl. 14(2), and 2011 — Behbahani and Lam, Strongly regular graphs with non-trivial automorphisms, Discrete Math. 311, 132–144: further restrictions on the possible automorphism groups.
2014/2017 — Conway's prize offer publicises the problem.

No graph with these parameters has been found, and no non-existence proof is known.

Setting

Fix a finite vertex set $V$ and a simple graph $g$ on $V$ (irreflexive, symmetric adjacency $\mathrm{Adj}$ ). For vertices $v,w$ write $N(v) = \{u : \mathrm{Adj}(v,u)\}$ for the neighbourhood of $v$ and $N(v)\cap N(w)$ for the set of common neighbours. The graph $g$ is strongly regular with parameters $(n,k,\lambda,\mu)$ , written $\mathrm{IsSRGWith}\ g\ n\ k\ \lambda\ \mu$ , when

$|V| = n$ ;
$|N(v)| = k$ for every vertex $v$ ;
$|N(v)\cap N(w)| = \lambda$ whenever $v$ and $w$ are adjacent;
$|N(v)\cap N(w)| = \mu$ whenever $v \neq w$ are non-adjacent.

The case $\lambda = 1$ says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are locally linear. The case $\mu = 2$ says that every non-adjacent pair is the pair of opposite corners of exactly one $4$ -cycle. Conway's problem asks for $(n,k) = (99,14)$ with these two local conditions.

Counting paths of length two from a fixed vertex gives $k(k-\lambda-1) = (n-k-1)\mu$ , which for $\lambda=1$ , $\mu=2$ reduces to $2n = k^2 + 2$ ; with $k = 14$ this yields $n = 99$ . Writing $A$ for the adjacency matrix, $I$ for the identity and $J$ for the all-ones matrix, strong regularity is equivalent to the matrix identity $A^2 = kI + \lambda A + \mu(J - I - A)$ , which for $(99,14,1,2)$ reads $A^2 + A = 12I + 2J$ ; the eigenvalues of $A$ other than $k=14$ are then $3$ and $-4$ , and integrality of their multiplicities ( $54$ and $44$ ) is one of the feasibility conditions that $(99,14,1,2)$ passes.

Formalization targets

Goal

\exists\ \alpha,\ \exists\ g \text{ a simple graph on } \alpha,\quad \mathrm{IsSRGWith}\ g\ 99\ 14\ 1\ 2 .

The goal is Mathlib's own proof_wanted conway_99 in Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters $(99,14,1,2)$ . A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.

Supporting targets

2n = k^2 + 2, \qquad k \text{ even}, \qquad k \in \{2,4,14,22,112,994\}

for every strongly regular graph with $\lambda = 1$ , $\mu = 2$ : the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.

\exists\, g,\ \mathrm{IsSRGWith}\ g\ 9\ 4\ 1\ 2, \qquad \exists\, g,\ \mathrm{IsSRGWith}\ g\ 243\ 22\ 1\ 2

the two members of the family that are known to exist: the $3\times 3$ rook's graph (the Paley graph on $9$ vertices) and the Berlekamp–van Lint–Seidel graph.

|E(g)| = 693, \qquad |\{\text{triangles of } g\}| = 231, \qquad A^2 + A = 12I + 2J, \qquad g \text{ not vertex-transitive}

structural consequences for a hypothetical $99$ -graph, the last one being Wilbrink's theorem.

Significance

A $(99,14,1,2)$ graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth $5$ with $99$ points and $231$ lines of size $3$ ; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions ( $\lambda=1$ , $\mu=2$ ) constrain global structure.

Nothing in this mission is presently formalized. Mathlib defines SimpleGraph.IsSRGWith, proves the counting identity IsSRGWith.param_eq, the complement rule IsSRGWith.compl, and the matrix identity IsSRGWith.matrix_eq, and records the $99$ -graph problem as a proof_wanted. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at $(9,4,1,2)$ and $(243,22,1,2)$ ; Wilbrink's non-vertex-transitivity; the integrality restriction on $k$ ); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of $k$ ); and the goal itself, which is open mathematics.

Difficulty

The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has $693$ edges among $\binom{99}{2} = 4851$ pairs, and no isomorph-free generation of locally linear graphs on $99$ vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at $(9,4,1,2)$ and $(243,22,1,2)$ . On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by $(99,14,1,2)$ , so a proof of non-existence needs an argument that does not factor through the parameters alone.

Formalization scope

All statements are phrased with Mathlib's SimpleGraph.IsSRGWith on a Fintype vertex type with DecidableRel adjacency, and use Fintype.card, SimpleGraph.edgeFinset, SimpleGraph.cliqueFinset 3 (triangles as $3$ -cliques), SimpleGraph.adjMatrix over $\mathbb{Z}$ , and graph isomorphisms g ≃g g for automorphisms. The goal quantifies over α : Type together with a Fintype α instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains $\lambda$ only through pairs that are actually adjacent and $\mu$ only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, $K_3$ ) do satisfy IsSRGWith with $\lambda = 1$ , $\mu = 2$ ; the supporting statements carry the cardinality hypotheses ( $0 < n$ , $1 < n$ ) that exclude them where needed, and the degenerate degree $k = 2$ is listed explicitly in the classification of feasible degrees.

Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the $(243,22,1,2)$ case; and decision procedures for strong regularity of an explicitly given small graph, for the $(9,4,1,2)$ case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.

Selected references

N. Biggs, Finite Groups of Automorphisms: Course Given at the University of Southampton, October–December 1969, London Mathematical Society Lecture Note Series 6, Cambridge University Press, 1971, p. 111.
E. R. Berlekamp, J. H. van Lint, J. J. Seidel, A strongly regular graph derived from the perfect ternary Golay code, in: A Survey of Combinatorial Theory, North-Holland, 1973, pp. 25–30.
R. K. Guy, Problems, in: The Geometry of Metric and Linear Spaces, Springer Lecture Notes in Mathematics 490, 1975, pp. 233–244 (Problem 7, J. J. Seidel, pp. 237–238). doi:10.1007/BFb0081147
H. A. Wilbrink, On the $(99,14,1,2)$ strongly regular graph, in: Papers dedicated to J. J. Seidel, EUT Report 84-WSK-03, Eindhoven University of Technology, 1984, pp. 342–355. PDF
A. E. Brouwer, A. Neumaier, A remark on partial linear spaces of girth 5 with an application to strongly regular graphs, Combinatorica 8 (1988), 57–61. doi:10.1007/BF02122552
A. A. Makhnev, I. M. Minakova, On automorphisms of strongly regular graphs with $\lambda=1$ , $\mu=2$ , Discrete Mathematics and Applications 14 (2004), no. 2. doi:10.1515/156939204872374
M. Behbahani, C. Lam, Strongly regular graphs with non-trivial automorphisms, Discrete Mathematics 311 (2011), 132–144. doi:10.1016/j.disc.2010.10.005
J. H. Conway, Five $1,000 Problems (Update 2017), OEIS. PDF

24 thms7 active usersReviewed

Operations Research Probability·Captain: Shuze Chen

The Komlos ConjectureOpen Problem

Motivation

Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.

Timeline

1963. Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show any norm admits a dimension-dependent bound $2d$ , setting the theme: how much of the dependence on dimension is real?
1981. Beck and Fiala (Discrete Appl. Math.) prove degree- $t$ set systems have discrepancy at most $2t - 1$ , by the floating-colors argument, and conjecture $O(\sqrt{t})$ .
1980s. Komlós poses the vector form — unit $\ell^2$ -norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's Ten Lectures (1987) as the central open problem of the area.
1985. Spencer (Trans. AMS) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
1998. Banaszczyk (Random Struct. Algorithms) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
2010–2016. The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg (STOC 2016) give a polynomial-time algorithm matching Banaszczyk's bound.
2023. Kunisky (SIAM J. Discrete Math.) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
2025. Bansal and Jiang (arXiv:2508.03961) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.

Setting

Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$ . A sign vector is an $\varepsilon \in \{-1, +1\}^n$ : one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$ -th coordinate of the vector $v_i$ , the discrepancy of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$ , the $\ell^\infty$ norm of the signed sum. The Komlós property at constant $K$ — KomlosBound K — says that every such family, in every $n$ and every $m$ , admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.

Set systems embed as the special case of $0/1$ -incidence matrices: if $A$ is an $m \times n$ matrix of $0$ s and $1$ s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.

Formalization targets

Goal — the Komlós conjecture

\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.

The goal fixes no value of $K$ : any finite universal constant settles it, so the statement survives every improvement in the constant.

Milestones — the known ladder

Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree- $t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$ "; Kunisky's lower bound $K \ge 1 + \sqrt{2}$ ; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$ .

Significance

The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.

None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.

Difficulty

Random signs lose: they give $\Theta(\sqrt{n})$ , not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.

Formalization scope

The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads ‖v i‖ ≤ 1); the $\ell^\infty$ conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise $0/1$ hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In beck_fiala the hypothesis $t \ge 1$ is required (the degree- $0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$ . In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$ .

Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.

Selected references

J. Beck, T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981). doi:10.1016/0166-218X(81)90022-6
J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985). doi:10.1090/S0002-9947-1985-0784009-0
W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998). doi link
N. Bansal, D. Dadush, S. Garg, An algorithm for Komlós conjecture matching Banaszczyk's bound, FOCS 2016 / SIAM J. Comput. arXiv:1605.02882
N. Bansal, H. Jiang, Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk, 2025. arXiv:2508.03961
D. Kunisky, The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant, SIAM J. Discrete Math. 37 (2023). arXiv:2111.02974
B. Chazelle, The Discrepancy Method, Cambridge University Press, 2000. author's page

24 thms7 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Convexity and Steinitz's Exchange Property II: The Local Supermodularity Theorem for the Concave ConjugateResearch Paper

Motivation

Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to $0/1$ vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).

The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.

Setting

Let $V$ be a finite nonempty set, $n=|V|$ . For $u\in V$ let $\chi_u\in\mathbb Z^V$ be the unit vector, for $X\subseteq V$ let $\chi_X$ be its characteristic vector, $x(X)=\sum_{v\in X}x(v)$ , and $\langle p,x\rangle=\sum_v p(v)x(v)$ . For a finite $B\subseteq\mathbb Z^V$ , $\overline B$ is its convex hull.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that

\text{(B1)}\quad x,y\in B,\ u\in\operatorname{supp}^+(x-y)\ \Rightarrow\ \exists v\in\operatorname{supp}^-(x-y):\ x-\chi_u+\chi_v\in B.

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC) (is M-concave) if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and $\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v)$ . Write $\omega[p](x)=\omega(x)+\langle p,x\rangle$ and $\operatorname{argmax}(g)$ for the maximizers of $g$ on $B$ .

The support function of $B$ is $\psi^\circ(p)=\min\{\langle p,x\rangle\mid x\in B\}$ . A positively homogeneous $h:\mathbb R^V\to\mathbb R$ is "matroidal" if

(C1) $X\mapsto h(\chi_X)$ is supermodular, and
(C2) $h(p)=\sum_{j=1}^n(p_j-p_{j+1})\,h(\chi_{V_j})$ whenever $V=\{v_1,\dots,v_n\}$ with $p(v_1)\ge\dots\ge p(v_n)$ , $p_j=p(v_j)$ , $V_j=\{v_1,\dots,v_j\}$ , $p_{n+1}=0$ .

The concave conjugate is $\omega^\circ(p)=\min\{\langle p,x\rangle-\omega(x)\mid x\in B\}$ , the concave closure is $\hat\omega(b)=\inf_p\{\langle p,b\rangle-\omega^\circ(p)\}$ , the subdifferential is $\partial\omega^\circ(p_0)=\{b\mid\omega^\circ(p)-\omega^\circ(p_0)\le\langle p-p_0,b\rangle\ \forall p\}$ , and the localization of $\omega^\circ$ at $p_0$ is $\hat L(\omega^\circ,p_0)(p)=\inf\{\langle p,b\rangle\mid b\in\partial\omega^\circ(p_0)\}$ .

Formalization targets

Goal: the Local Supermodularity Theorem (Theorem 5.3, corrected)

For $\omega$ on a finite integral base set $B$ ,

\omega\ \text{satisfies (EXC)}\iff\Big(\omega=\hat\omega\ \text{on}\ B\Big)\ \text{and}\ \Big(\hat L(\omega^\circ,p_0)\ \text{is "matroidal" for every}\ p_0\in\mathbb R^V\Big).

The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: $B=\{(2,0),(1,1),(0,2)\}$ , $\omega=(0,-10,0)$ .

Milestones

Theorem 2.1: (B1) is equivalent to $B$ being the integer points of an integral submodular (equivalently, supermodular) system, whose defining function is determined by $B$ .
Theorem 5.1: if $B=\mathbb Z^V\cap\overline B$ , then $B$ satisfies (B1) iff $\psi^\circ$ is "matroidal".
Lemma 5.2: sums of "matroidal" functions are "matroidal".
Theorem 4.4: (EXC) holds iff every $\operatorname{argmax}(\omega[p])$ satisfies (B1).
Eq. (5.12): $\hat L(\omega^\circ,p_0)(p)=\min\{\langle p,x\rangle\mid x\in\operatorname{argmax}(\omega[-p_0])\}$ .

Significance

The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of $\omega^\circ$ , in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.

The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of $\operatorname{conv}(\operatorname{argmax}\,\omega[-p_0])$ to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.

Difficulty

$\omega^\circ$ depends only on the concave closure $\hat\omega$ , so any characterization of (EXC) through $\omega^\circ$ alone cannot see values of $\omega$ below $\hat\omega$ . That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near $p_0$ .

Formalization scope

Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of $\mathbb Z^V$ is a Finset (V → ℤ). A function on $B$ is a total function (V → ℤ) → ℝ whose values off $B$ are never used. The mission commits to the following readings:

Minima. $\psi^\circ$ , $\omega^\circ$ are real infima over the finite set $B$ , hence minima for nonempty $B$ (every statement has $B$ nonempty). $\hat\omega$ is a real infimum used only at points of $B$ , where it is bounded below.
Localization. $\hat L$ is a real sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.
(C2). It is required for every bijection Fin n ≃ V along which $p$ is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.
Theorem 2.1. The page's " $\forall X\subset V$ " is read as all $X\subseteq V$ . The set functions are integer-valued, and "Moreover" is read strongly: every $f$ (resp. $g$ ) as in (b) (resp. (c)) equals the displayed max (resp. min).
Theorem 4.4. " $\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope" is read as " $\operatorname{argmax}(\omega[p])$ satisfies (B1)", following Lemma 4.3 and the proof of Theorem 5.3. The literal convex-hull reading makes the "if" direction false (same counterexample).
Theorem 5.1 keeps the page's hypothesis $B=\mathbb Z^V\cap\overline B$ .

Trivializing formalizations are ruled out. Defining $\hat L$ by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An $\omega^\circ$ taken as a supremum would reverse the sign conventions.

The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.

Selected references

K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996), 272–311. https://doi.org/10.1006/aima.1996.0084
A. W. M. Dress, W. Wenzel, Valuated matroids: a new look at the greedy algorithm, Applied Mathematics Letters 3 (1990), 33–35.
S. Fujishige, Submodular Functions and Optimization, 2nd ed., Annals of Discrete Mathematics 58, Elsevier, 2005.
L. Lovász, Submodular functions and convexity, in Mathematical Programming: The State of the Art, Springer, 1983, 235–257. https://doi.org/10.1007/978-3-642-68874-4_10
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

15 thms6 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Cores of Convex Games: The Core of a Convex Game Is Its Unique von Neumann-Morgenstern Stable SetResearch Paper

Motivation

A cooperative game with transferable utility assigns to every coalition of players the total payoff the coalition can secure on its own. Two solution concepts for such games go back to the foundations of game theory: the core, the set of payoff divisions no coalition can improve upon, and the stable set (von Neumann–Morgenstern solution), a set of divisions that is internally consistent and externally absorbing under the relation of domination. For general games the two concepts behave badly: the core may be empty, stable sets may fail to exist (Lucas 1968), and when they exist there are usually many of them.

Lloyd Shapley's paper Cores of Convex Games (Int. J. Game Theory 1, 1971) isolates a class of games, the convex games (supermodular characteristic functions), on which all of this becomes well behaved. Convex games arise in cost allocation, in bankruptcy and airport problems, in scheduling and sequencing games, and in any setting with increasing returns to cooperation; the supermodular functions behind them are the same objects studied as polymatroid rank functions in combinatorial optimization (Edmonds 1970). For such games the paper shows that the core is nonempty, that its faces fit together in a rigid combinatorial pattern, that its vertices are exactly the marginal-contribution vectors, and that the core is the unique stable set.

Setting

Let $N=\{1,\dots,n\}$ be a finite set of players. A game is a function $v$ from subsets of $N$ to the reals with $v(\emptyset)=0$ . It is convex if

v(S)+v(T)\le v(S\cup T)+v(S\cap T)\qquad\text{for all } S,T\subseteq N.

A payoff vector is $a\in\mathbb R^N$ , and $a(S)=\sum_{i\in S}a_i$ . It is feasible if $a(N)\le v(N)$ . The core $C$ is the set of feasible $a$ with $a(S)\ge v(S)$ for every $S\subseteq N$ ; in particular $a(N)=v(N)$ on $C$ .

For a nonempty coalition $S$ , the face $C_S$ is the set of core points with $a(S)=v(S)$ ; by convention $C_\emptyset=C$ , and $C_N=C$ . The family $\{C_S\}$ is the core configuration. It is complete if no $C_S$ is empty, and regular if $C_N\ne\emptyset$ and

C_S\cap C_T\subseteq C_{S\cup T}\cap C_{S\cap T}\qquad\text{for all } S,T\subseteq N.

For an ordering $\omega$ of the players, $S_{\omega,k}$ is the set of the first $k$ players, and the marginal vector $a^\omega$ pays each player $i$ its marginal contribution $v(S_{\omega,\omega(i)})-v(S_{\omega,\omega(i)-1})$ .

A payoff vector $b$ is dominated by $a$ if some nonempty coalition $S$ has $a(S)\le v(S)$ and $a_i>b_i$ for all $i\in S$ . A set $V$ of feasible vectors is stable if every feasible vector is either a member of $V$ or dominated by a member of $V$ , but not both.

Formalization targets

Goal: Theorem 8

C \text{ is stable, and every stable set } V \text{ equals } C \qquad (v \text{ convex}).

The goal contains both halves of the page's statement: stability of the core, and uniqueness ("the unique von Neumann–Morgenstern solution").

Milestones, in the order the argument uses them

Lemma 1 (p. 18) and Lemma 2 (p. 19): for a regular configuration, a point on two nested faces $C_S\cap C_T$ with $|T\setminus S|\ge2$ can be moved to a face $C_Q$ of an intermediate coalition, and a point of $C_S$ to $C_S\cap C_{S\cup\{j\}}$ , keeping its coordinates on $S$ .
Theorem 2 (p. 18): in a regular configuration $C_{S_1}\cap\cdots\cap C_{S_m}\ne\emptyset$ for every strictly increasing chain $S_1\subset\cdots\subset S_m$ ; in particular a regular configuration is complete.
Theorem 4 (p. 21): the core of a convex game is nonempty.
Theorem 5 (p. 22): a game is convex if and only if its core configuration is regular.
Two claims of §4.3 (p. 24): every stable set contains the core, and no stable set properly includes another.
The claim that opens the proof of Theorem 8 (p. 24): in a convex game every feasible vector outside the core is dominated by a core point.

The mission also states Theorem 3 (p. 19), the vertices of a regular core are exactly the marginal vectors $a^\omega$ , as a further item that is not on the path to the goal.

Significance

The result. Theorem 8 gives, for a natural and widely occurring class of games, a complete answer to the existence and uniqueness questions for von Neumann–Morgenstern solutions, which are open or negative in general. Theorems 3 and 5 describe the core of a convex game explicitly as the polytope spanned by the $n!$ marginal vectors, the combinatorial description that underlies later work on the Shapley value, the Weber set, and the polymatroid greedy algorithm. Theorem 5 is the geometric characterization of supermodularity through the face structure of the core.

Formalizing it. All results in this mission are proved in the paper; none has a machine-checked proof on the platform. Theorem 4 is already stated on the platform (as part of a statement that also puts every marginal vector and the Shapley value in the core) and enters the mission as an existing item. The remaining work is a formal development of face configurations of the core, of stable sets and domination, and of the passage from supermodularity to the geometry of the core. The definitions of stable set and domination are general and reusable for any transferable-utility game.

Difficulty

The internal half of stability is immediate from the definitions: a core point cannot be dominated by any vector satisfying a coalition constraint $a(S)\le v(S)$ . Uniqueness also follows from two short observations. The substance is external stability: every feasible vector outside the core must be dominated by a core point, and the dominating vector has to be produced explicitly. The obvious attempt, raising the payoffs of one violated coalition and leaving the other coordinates of $b$ unchanged, does not in general produce a core point, and nothing in the definition of the core alone controls how the core meets the hyperplane of a given coalition; that control is what the face theory of §3 is about. For non-convex games the external half genuinely fails, so no argument that ignores convexity can succeed.

Formalization scope

Players are Fin n (a relabelling of the paper's finite set $N$ ), a game is f : Finset (Fin n) → ℝ, payoff vectors are Fin n → ℝ, and $a(S)$ is ∑ i ∈ S, a i. The existing platform definitions Supermodularity.Cooperative.IsConvexGame ( $v(\emptyset)=0$ plus supermodularity on all subsets), Core, InitialCoalition and GreedyPayoff (the marginal vectors, orderings being permutations of Fin n) are reused; the reused Theorem 4 statement is Supermodularity.Cooperative.convex_game_core_and_shapley.

Conventions committed to:

Wherever the page says "a game", the hypothesis is exactly $v(\emptyset)=0$ ; convexity is IsConvexGame.
Faces satisfy $C_\emptyset=C$ literally: the tightness condition is imposed only for nonempty $S$ .
Regularity includes $C_N\ne\emptyset$ , as on the page.
Lemmas 1–2 and Theorems 2–3 assume a regular configuration, not convexity, as on the page.
$S\subset\subset T$ is $S\subsetneq T$ with $|T|-|S|\ge2$ ; Lemma 1's two preassigned elements are distinct.
An increasing sequence of $m\ge1$ coalitions is a strictly monotone map from Fin (m + 1).
"Vertex" is Set.extremePoints ℝ.
Domination requires a nonempty coalition and strict coordinate inequalities; stable sets consist of feasible vectors and the "either … or …, but not both" condition ranges over feasible vectors, following the page rather than the classical imputation-based variant.

A formalization in which the dominating coalition may be empty, in which regularity omits $C_N\ne\emptyset$ , or in which the goal asserts stability without uniqueness does not state the paper's theorem and is ruled out.

Welcome contributions: proofs of the milestones in any order, general lemmas about faces of polytopes cut out by set-function inequalities, and reusable API for domination and stable sets.

Selected references

L. S. Shapley, Cores of Convex Games, International Journal of Game Theory 1 (1971), 11–26. https://doi.org/10.1007/BF01753431
J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87. https://doi.org/10.1007/3-540-36478-1_2
W. F. Lucas, A game with no solution, Bulletin of the American Mathematical Society 74 (1968), 237–239. https://doi.org/10.1090/S0002-9904-1968-12039-2
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998, §5.2.

20 thms6 active usersReviewed

Completed

Number Theory·Captain: aarontcao

Long-Wagner Conjecture 5.1: cube-free subsets of Z/2^nZ have density at most 5/8Open Problem

Call $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ cube-free if no triple $x, y, z$ has all seven of $x$ , $y$ , $z$ , $x+y$ , $y+z$ , $z+x$ , $x+y+z$ inside $A$ . The triple is unconstrained, so a degenerate one counts. Write $f(n)$ for the largest size of a cube-free subset.

The conjecture. $f(n) \le \frac{5}{8} 2^n$ for every $n$ .

This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of $\mathbb{Z}_{2^n}$ , arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.

The constant is attained

The bound is sharp, and the extremal set is explicit: $A = \{v : v \bmod 8 \in \{1,3,4,5,7\}\}$ , the odd residues together with those congruent to 4 mod 8. Its size is $2^{n-1} + 2^{n-3} = \frac{5}{8} 2^n$ . In the layer language of Long and Wagner this is $C_3 = L_1 \cup L_3$ .

What is known

The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at $d = 3$ , and it is the largest class on which the conjectured constant is proved.

For arbitrary sets the best published unconditional bound is $f(n) < \frac{2}{3} 2^n$ . Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward $5/8$ . The residual gap is exactly $\frac{2}{3} - \frac{5}{8} = \frac{1}{24}$ , that is $2^n/24$ elements.

Small values are $f(1) = 1$ , $f(2) = 2$ , $f(3) = 5$ , $f(4) = 10$ , $f(5) = 20$ , $f(6) = 40$ , $f(7) = 80$ , matching $2^{n-1} + 2^{n-3}$ from $n = 3$ on.

State those values honestly. They come from solver searches, Gurobi in Long and Wagner for $n \le 7$ and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at $n = 7$ ", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So $f(7) \ge 80$ is solid and $f(7) \le 80$ is not certified. Nothing in this mission rests on either.

What the items are

The goal item is the conjecture itself, for $n \ge 4$ , and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances $n = 4$ and $n = 5$ are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.

The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then $n = 4$ and $n = 5$ .

Notes on the formalization

Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves $0$ in no layer at all and needs the last layer special-cased.

CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.

18 thms6 active usersReviewed

Completed

Graph Theory Theoretical Computer Science·Captain: hao jia

Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper

Motivation

A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.

Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune $14$ -regular bipartite graph of at least that girth, and it has a perfect matching.

This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.

Setting

For a finite simple graph $G$ and a vertex set $A\subseteq V(G)$ , the associated cut consists of all edges with one endpoint in $A$ and one in $V(G)\setminus A$ . The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.

The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is $14$ -regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.

The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, $K_1$ has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.

Formalization targets

Lemma 5 — immune high-girth graphs

The main theorem follows the paper's structural lemma:

\forall g\ge3\ \exists G, \quad G\text{ is finite, connected, bipartite, and $14$-regular},

\operatorname{girth}(G)\ge g, \qquad G\text{ has no matching cut}, \qquad G\text{ has a perfect matching}.

The graph may depend on $g$ . The existence quantifier does not request an efficient algorithm or a numerical order bound.

Negative OPG consequence

A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:

\forall g\ge3\ \exists G, \qquad \overline d(G)=14<15, \quad \operatorname{girth}(G)\ge g, \quad G\text{ has no matching cut}.

Thus choosing $d=15$ refutes the intended universal assertion that some girth threshold works for every graph of average degree below $d$ .

Significance

The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.

Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every $g\ge3$ , Matching Cut is NP-complete even for bipartite graphs of girth at least $g$ and maximum degree at most $60$ . Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.

Difficulty

Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.

A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.

Formalization scope

Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least $g$ means every such cycle has length at least $g$ , so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.

The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the $K_1$ ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.

Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.

Selected references

C. Feghali, F. Lucke, D. Paulusma, and B. Ries, Matching Cuts in Graphs of High Girth and H-Free Graphs, Algorithmica 87 (2025), 1199–1221. https://doi.org/10.1007/s00453-025-01318-8
C. Feghali, F. Lucke, D. Paulusma, and B. Ries, ISAAC 2023 version. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.31
A. Lubotzky, R. Phillips, and P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988), 261–277. https://doi.org/10.1007/BF02126799
Open Problem Garden, Matching cut and girth. https://www.openproblemgarden.org/op/matching_cut_and_girth

20 thms6 active usersReviewed

Completed

Graph Theory·Captain: hao jia

Formalizing an 8-Vertex Candidate Counterexample to the Geodesic-Cycle Assignment Problem (OPG-500)Open Problem

[VM-STATUS-20260908-R05-PROVED]

Status update (2026-09-08): The root theorem OPG500Counterexample.eight_vertex_counterexample is now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.

Motivation and historical context

Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.

Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.

The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.

Setting

Let $G$ be a finite simple graph. A positive edge-length assignment is a function

\ell:E(G)\longrightarrow \mathbb R

such that $\ell(e)>0$ for every edge $e$ . The length of a finite path or cycle is the sum of the lengths of its edges.

A simple cycle $C$ is $\ell$ -geodesic when, for every pair of vertices $x,y$ on $C$ , at least one of the two $x$ – $y$ arcs of $C$ has length equal to the shortest-path distance between $x$ and $y$ in $G$ . Equivalently, there is no $x$ – $y$ path in $G$ whose length is strictly smaller than both $x$ – $y$ arcs of $C$ . The definition concerns vertices of the cycle and permits ties between shortest paths.

A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.

Fix the graph $H$ on vertices $0,1,\ldots,7$ . The vertices $0,1,2,3$ induce $K_4$ . For each $i\in\{0,1,2,3\}$ , set $y_i=7-i$ and join $y_i$ to exactly the three core vertices other than $i$ . The four vertices $y_i$ are pairwise nonadjacent. Thus the frozen edge set is

\{01,02,03,04,05,06,12,13,14,15,17,23,24,26,27,35,36,37\}.

The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.

Formalization targets

Main target: the universal eight-vertex obstruction

Formalize the following statement for the fixed graph $H$ :

H\text{ is 3-connected}\quad\text{and}\quad \forall\ell:E(H)\to\mathbb R_{>0},\; \exists C,\; C\text{ is an $\ell$-geodesic simple cycle of $H$ and is not peripheral}.

The existential cycle may depend on $\ell$ . The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.

Supporting targets

The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of $H$ , the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.

Significance

A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.

A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.

Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.

Difficulty

The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.

The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.

Formalization scope

The Lean development will use Fin 8 for the vertices of $H$ and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.

The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.

Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.

Selected references

A. Georgakopoulos and P. Sprüssel, Geodetic topological cycles in locally finite graphs, Electronic Journal of Combinatorics 16 (2009), R144. Section 3.1, Theorem 3.1; Section 5, Problem 3. https://arxiv.org/abs/0911.3999v1
Open Problem Garden, Geodesic cycles and Tutte's Theorem, problem statement and vertex-based definition. https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem
W. T. Tutte, How to draw a graph, Proceedings of the London Mathematical Society 13 (1963), 743–768. Cited as reference [18] by Georgakopoulos and Sprüssel for peripheral-cycle generation.
Vibe Mathing, frozen OPG-500 candidate repository at commit a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924

9 thms6 active usersReviewed

Completed

Discrete Geometry·Captain: mysticflounder

Erdős Problems 97 and 96: Convex Point Sets and Unit DistancesOpen Problem

Closed — negative resolution of Erdős Problems 96 and 97

Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.

Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.

Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.

Historical mission description

Motivation

The mission is to prove the combined open goal

\text{Problem 97} \;\land\; \text{Problem 96}

for finite point sets in strictly convex position in the Euclidean plane.

Why Problems 97 and 96 belong together

Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius $1$ . Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an $n$ -point set determines at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound and therefore $O(n)$ . The package uses this one-way dependency; it does not seek a reverse implication.

Setting

Let $A\subset\mathbb R^2$ be finite. Strict convex position means that every point of $A$ is an extreme point of the convex hull of $A$ . For $p\in A$ , the pinned multiplicity at radius $r>0$ counts points $q\in A$ with $\lVert p-q\rVert=r$ . Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance $1$ , then takes the supremum over convex-independent $n$ -point sets.

The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.

Target

The Problem 97 target is the canonical statement that every nonempty finite convex-independent $A$ has no four-equidistant-point property:

\forall A,\quad A\ne\varnothing\;\to\;\operatorname{ConvexIndep}(A) \;\to\;\neg\operatorname{HasNEquidistantProperty}(4,A).

The Problem 96 target is the canonical asymptotic statement

U_c(n)=O(n),

where $U_c(n)$ is the supremum of the unordered unit-distance counts determined by convex-independent $n$ -point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$ for every natural number $n$ .

Significance

The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant $3$ , while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.

Difficulty

The source proof reduces Problem 97 to strong induction on $|A|$ . Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.

Counterexample routes

Problem 97 is open, so the mission also records the parallel negative route. The source formalization calls a nonempty convex-independent finite set with the four-equidistant property a Problem97.IsCounterexample. Constructing one such set would refute Problem 97 and therefore refute the mission's affirmative conjunction, regardless of whether Problem 96 remains true. The counterexample milestone keeps this resolution path visible beside the nonexistence proof. A successful witness must use exact coordinates or exact algebraic data from which Lean verifies both strict convex position and the four-equidistant property; a numerical approximation or a realizable incidence pattern alone is insufficient.

Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.

Formalization scope

The canonical source is pinned at commit 757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source statements for Problem 97 and Problem 96. The source repository reports closed proofs of the conditional bridge to the $3n$ bound (conditional three-times bound), the $|A|\ge9$ counting milestone (nine-point counting bound), and the exact nine-point exclusion (exact nine-point exclusion theorem). The remaining large-cardinality milestone is the removable-vertex step, with its minimality hypothesis retained. The current platform mission contains accepted transfers of the counting argument, the conditional bridge, and the exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make convex independence and the positive-radius condition explicit; no theorem is assumed inside a definition. Singletons and two-point sets are included in Problem 97, while Problem 96's counting definitions also include the empty set. The source repository uses Lean v4.27.0; these mission statements target the platform's v4.33.1. Source-proof transfer and revalidation remain separate work. The Lean declarations and proofs are this project's own formalization. The Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical provenance; they do not indicate that a paper proof was imported or machine-checked directly.

These source results establish the intended dependency graph: the P97 universal root feeds low-unit-degree extraction, strong induction, and then the P96 supremum bound. The platform mission records those contracts and milestones; it does not claim to have transplanted their proof bodies. The milestones include the two canonical roots, their conditional bridge, the |A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step, the documented Danzer nine-point three-neighbor example, the parallel goal of constructing a Problem 97 counterexample, and the superlinear-family route to a counterexample to Problem 96.

References

Erdős, On Sets of Distances of n Points (1946), DOI.
Erdős, Some Combinatorial and Metric Problems in Geometry (1987), scan.
Fishburn–Reeds, Unit Distances Between Vertices of a Convex Polygon (1992), publisher record.
Dumitrescu, On Distinct Distances from a Vertex of a Convex Polygon (2006), Springer record; provenance for the source counting method.
Nivasch–Pach–Pinchasi–Zerbib, The Number of Distinct Distances from a Vertex of a Convex Polygon (2013), arXiv:1207.1266; provenance for the cap-witness refinements used by the source formalization.

80 thms6 active usersReviewed

Completed

Number Theory·Captain: ShouqiaoWang

Erdős Problem 390: Exact Second-Order AsymptoticResearch Paper

Determine the exact second-order term in the least possible largest factor in a factorization of $n!$ into distinct integers exceeding $n$ , with the proposed rational constant $4029639598/25970038185$ .

97 thms6 active usersReviewed

Completed

Graph Theory·Captain: mikedeng1

Applied Combinatorics I: Graph Theory and Dirac's Hamiltonicity TheoremTextbook

Motivation

Graphs are the most basic combinatorial model of pairwise relations: road networks, frequency interference between radio stations, schedules, circuit layouts. Chapter 5 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) introduces the vocabulary of graph theory and proves its first structural theorems: when a graph can be traversed edge by edge (Euler, 1736), when it can be toured vertex by vertex (Dirac, 1952), when it can be colored with two colors, and how far the chromatic number can drift from the size of the largest clique.

Hamiltonicity is the vertex analogue of Euler's edge-traversal problem and behaves very differently: Euler's problem has a simple parity characterization, while deciding whether a graph has a hamiltonian cycle is NP-complete (Karp, 1972). Sufficient conditions are therefore the main tool, and the minimum-degree condition of Dirac (1952) is the first and most cited of them; Ore's condition (1960) and the Bondy–Chvátal closure (1976) refine it.

Setting

A graph $G = (V, E)$ consists of a finite vertex set $V$ and a set $E$ of 2-element subsets of $V$ , the edges; $xy \in E$ means $x$ and $y$ are adjacent. The degree $\deg_G(v)$ is the number of neighbours of $v$ . The mission uses Mathlib's SimpleGraph V with [Fintype V]; "a graph on $n$ vertices" means Fintype.card V = n.

A cycle is a sequence $(x_1, \dots, x_n)$ of $n \ge 3$ distinct vertices with $x_i x_{i+1} \in E$ for $i < n$ and $x_1 x_n \in E$ ; its length is $n$ . A graph is acyclic if it has no cycle, and a tree if it is connected and acyclic. A leaf of a tree is a vertex of degree $1$ .
A hamiltonian cycle is a sequence $(x_1, \dots, x_n)$ in which every vertex appears exactly once, $x_i x_{i+1} \in E$ for $i < n$ , and $x_1 x_n \in E$ . A graph is hamiltonian if it has one (AppliedComb.Graphs.IsHamiltonian).
An eulerian circuit is a sequence $(x_0, \dots, x_t)$ , repetition allowed, with $x_0 = x_t$ , consecutive entries adjacent, and every edge equal to $x_i x_{i+1}$ for exactly one $i < t$ . A graph without isolated vertices is eulerian if it has one (IsEulerian).
A proper coloring assigns colors to vertices so that adjacent vertices differ; the chromatic number $\chi(G)$ is the least number of colors in a proper coloring, and the clique number $\omega(G)$ is the largest size of a set of pairwise adjacent vertices.
An interval graph is the intersection graph of closed intervals $[a_v, b_v] \subset \mathbb R$ , $v \in V$ : distinct $u, v$ are adjacent iff their intervals meet (IsIntervalGraph).

Formalization targets

Goal: Dirac's theorem (Theorem 5.18)

\text{If } |V| = n \ge 1 \text{ and } \deg_G(v) \ge \left\lceil \tfrac n2 \right\rceil \text{ for all } v \in V, \text{ then } G \text{ is hamiltonian.}

Milestones

In the book's order:

Proposition 5.11. A tree on $n \ge 2$ vertices has at least two leaves.
Theorem 5.13 (Euler). A graph without isolated vertices is eulerian if and only if it is connected and every degree is even.
Theorem 5.21. $\chi(G) \le 2$ if and only if $G$ contains no odd cycle.
Proposition 5.24 (generalized pigeonhole). If $f : X \to Y$ and $|X| \ge (m-1)|Y| + 1$ , some fibre of $f$ contains $m$ distinct elements.
Proposition 5.25. For every $t \ge 3$ there is a finite graph $G_t$ with $\chi(G_t) = t$ and $\omega(G_t) = 2$ .
Theorem 5.28. Every finite interval graph satisfies $\chi(G) = \omega(G)$ .

The book's proof of Theorem 5.18 uses only the pigeonhole principle, so none of these results lies on its path. The milestones are the chapter's other theorems about the same objects (cycles, degrees, colorings), and they share the goal's definitions. Cayley's formula (Theorem 5.39, $n^{n-2}$ labelled trees on $n$ vertices) is already on the platform as GYGraphTheory.cayley_tree_formula and is included as a reference item.

Significance

Dirac's theorem is sharp: the complete bipartite graph $K_{k,k+1}$ has minimum degree $k = \lceil n/2 \rceil - 1$ and no hamiltonian cycle. It is the starting point for the theory of degree conditions for hamiltonicity (Ore, Pósa, Chvátal) and for its extremal and random-graph analogues. Euler's theorem gives linear-time recognition of eulerian graphs; Theorem 5.21 characterizes bipartite graphs; Proposition 5.25 shows that local sparsity (no triangles) does not bound the chromatic number; Theorem 5.28 is the first step towards perfect graphs.

All of these results have been proved for a long time. What is missing is their formalization. Mathlib provides SimpleGraph, chromaticNumber, cliqueNum, degree-sum identities, and definitions of eulerian and hamiltonian walks. It contains no Dirac theorem, no converse of the eulerian degree condition, and no interval-graph theory. On the platform, FamousTheorems.two_colorable_iff_no_odd_cycle_6b is stated with odd closed walks rather than odd cycles, and triangle_free_chromatic_number asserts only $\chi \ge k$ rather than $\chi = t$ with $\omega = 2$ exactly.

Difficulty

For Dirac's theorem the obvious approach, induction on $n$ (deleting a vertex), fails: deleting a vertex lowers degrees, and the hypothesis $\deg \ge \lceil n/2 \rceil$ is not inherited by the smaller graph. The degree condition is global, and so is the argument that uses it. In Lean the argument also has to reverse and splice vertex sequences while keeping distinctness and every adjacency along the way. The sufficiency half of Euler's theorem has to construct a circuit that uses every edge exactly once, not just show that one exists up to parity. In Theorem 5.21 the obstruction is a cycle with distinct vertices; producing one from a failed 2-coloring takes more work than producing an odd closed walk. Proposition 5.25 needs a concrete infinite family of graphs and exact computation of both invariants. The upper bound $\chi \le t$ is easy, but the lower bound $\chi \ge t$ is not.

Formalization scope

Graphs are SimpleGraph V on a Fintype V. The number of vertices is always Fintype.card V, never a free parameter; in Theorem 5.18 the ceiling $\lceil n/2 \rceil$ is (n + 1) / 2 in $\mathbb N$ , with Fintype.card V = n.
"Hamiltonian" is the book's definition (p. 79), a list of all vertices without repetition with consecutive and first/last entries adjacent. It is not Mathlib's Walk.IsHamiltonianCycle, which needs at least three vertices: under that notion Theorem 5.18 would be false for $K_2$ . The goal assumes $V$ nonempty, as the book's proof does ( $n$ positive). Degenerate readings are ruled out: a predicate satisfied by a cycle through only some vertices, or a statement in which $n$ is not the number of vertices, would make the goal vacuous or false, and neither is used here.
"Eulerian" follows p. 75. Since the book defines it only for graphs without isolated vertices, Theorem 5.13 carries that hypothesis explicitly.
Cycles are the book's cycles (distinct vertices, length $\ge 3$ ), not closed walks. Theorem 5.21 is stated with odd cycles.
$\chi$ is Mathlib's chromaticNumber ( $\mathbb N_\infty$ -valued) and $\omega$ is cliqueNum; on finite graphs both agree with the book's definitions (pp. 81, 84).
Planarity (Section 5.5: Euler's formula 5.32, the bound $3n - 6$ in 5.33, Kuratowski 5.34, the Four Color Theorem 5.37) is excluded. The book defines planar drawings through polygonal arcs in $\mathbb R^2$ and faces, which is a topological development rather than a chapter mission. Kuratowski's theorem and the Four Color Theorem are not proved in the book.
Contributions reusable beyond this mission are welcome: path/cycle manipulation lemmas for list-based sequences, the Euler circuit construction, bipartiteness via distance parity, and the Mycielski construction.

Selected references

M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 5. https://www.appliedcombinatorics.org/
G. A. Dirac, Some theorems on abstract graphs, Proc. London Math. Soc. (3) 2 (1952), 69–81. https://doi.org/10.1112/plms/s3-2.1.69
L. Euler, Solutio problematis ad geometriam situs pertinentis, Commentarii Academiae Scientiarum Petropolitanae 8 (1741), 128–140 (read 1736). https://scholarlycommons.pacific.edu/euler-works/53/
J. Mycielski, Sur le coloriage des graphs, Colloquium Mathematicum 3 (1955), 161–162. https://doi.org/10.4064/cm-3-2-161-162
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations (1972), 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9

12 thms5 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Competitive Paging Algorithms IV: An Algorithm Competitive against Several Others Exists iff the Reciprocal Ratios Sum to at Most 1Research Paper

Motivation

Paging is the problem of managing a fast memory that holds $k$ pages out of $n$ : when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be $k$ times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is $2H_k$ -competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).

The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.

Setting

A type $(k,n)$ consists of $k$ servers and a finite set $M$ of $n$ vertices with the uniform metric: two distinct vertices are at distance $1$ . This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.

A deterministic on-line algorithm $A$ of type $(k,n)$ has an initial configuration of its $k$ servers and, after each request $r\in M$ , moves servers so that some server covers $r$ ; its configuration after a request sequence depends only on that sequence. Its cost $C_A(\sigma)$ on a request sequence $\sigma$ is the total distance its servers travel, i.e. the number of server moves.

For algorithms $A$ and $B$ of the same type and a constant $c$ , $A$ is $c$ -competitive against $B$ if there is a constant $a$ such that for every request sequence $\sigma$

C_A(\sigma)\le c\cdot C_B(\sigma)+a .

A sequence $c^*=(c(1),\dots,c(m))$ of positive reals is realizable if for every type $(k,n)$ and every $m$ deterministic on-line algorithms $B(1),\dots,B(m)$ of that type there is a deterministic on-line algorithm $A$ of the same type that is $c(i)$ -competitive against $B(i)$ for every $i$ .

Formalization targets

Goal: Theorem 6

For $m\ge1$ and positive reals $c(1),\dots,c(m)$ ,

c^*\ \text{is realizable}\iff \sum_{1\le i\le m}\frac1{c(i)}\le 1 .

Milestones

In the order of the paper's proof:

Punishments are paid for. If $A$ punishes $B$ at a time step (an $A$ -interval on a vertex $v$ ends at that step and contains the end of a $B$ -interval on $v$ that began no later), then $B$ has moved a server; the number of such steps is at most $C_B(\sigma)$ .
A fault leaves room to punish. If $|S_A|=k$ , $|S_B|\le k$ , $x\in S_B$ and $x\notin S_A$ , then some $u\in S_A$ is not in $S_B$ .
The greedy quota claim. If $\sum_i 1/c(i)\le 1$ and each unit of cost punishes the $B(i)$ minimizing $c(i)(\mathrm{PUN}(i)+1)$ (other algorithms may be punished incidentally), then after cost $r$ every $B(i)$ has been punished at least $\lfloor r/c(i)\rfloor$ times.
Shuttle algorithms. With $2m-1$ servers on $2m$ vertices there are $m$ algorithms, each keeping all vertices outside its own pair covered, no two of which move at the same step; in particular their total cost on any $\sigma$ is at most $|\sigma|$ .
A forcing adversary. With $2m-1$ servers on $2m$ vertices every algorithm can be forced to move at each of $N$ steps, so $C_A(\tau(N))\ge N$ .

Significance

The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is $\{c:\sum 1/c(i)\le 1\}$ . For example, any two paging algorithms can be combined into one that is $2$ -competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's $2H_k$ worst-case guarantee can be obtained within constant factors by one algorithm.

Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.

Difficulty

Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the $B(i)$ and follow one of them: switching between their configurations costs up to $k$ per switch, which no additive constant absorbs. The accounting has to charge each of $A$ 's faults to a specific move of a specific $B(i)$ , and the charge must be injective; the paper's claim that $C_B(\sigma)$ is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly $\sum 1/c(i)\le 1$ , and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first $k$ faults of $A$ (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.

Necessity needs the right family of hard instances: the $m$ algorithms must never move at the same step, which pins the type to $(2m-1,2m)$ .

Formalization scope

The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:

a type $(k,n)$ is any k : ℕ and any finite M : Type with a metric in which distinct points are at distance $1$ ; realizability quantifies over all of them, never over one fixed type;
servers are labelled; each algorithm has its own initial configuration, and the additive constant $a$ is chosen before the request sequence;
$c(i)>0$ and $m\ge1$ are hypotheses of the goal, as in the paper; without positivity, $1/0=0$ in Lean would make a zero ratio free;
time $t$ is the step processing the $t$ -th request; the paper's $\mathrm{PUN}$ counts time steps.

Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.

A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the $B(i)$ 's configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.

Selected references

A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. doi:10.1016/0196-6774(91)90041-V; preprint arXiv:cs/0205038.
D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2):202–208, 1985. doi:10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11(2):208–230, 1990. doi:10.1016/0196-6774(90)90003-W

9 thms5 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research+1·Captain: mikedeng1

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 3: Capacity Scaling for the Hitchcock ProblemResearch Paper

Motivation

The Hitchcock transportation problem asks how to ship a commodity from $m$ supply points to $n$ demand points at minimum total cost. It was posed by Hitchcock in 1941 and is one of the founding problems of linear programming and network optimization; it is solved routinely in logistics, and its structure (a bipartite network with supplies, demands and per-unit costs) recurs in assignment, optimal transport and matching.

The classical algorithms for it, the Ford–Fulkerson primal–dual method among them, augment flow one path at a time. With integral data their number of augmentations is bounded only by the total supply $\sum_i a_i$ , which is exponential in the number of binary digits used to write the data. Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems (J. ACM 19(2), 1972, doi:10.1145/321694.321699), introduced capacity scaling: solve a coarse version of the problem first, then refine one binary digit at a time. Their Theorem 9 (p. 260) bounds the total number of augmentations by a quantity proportional to $\max(m,n)$ times the number of bits of the data, which made the transportation problem, and through standard reductions the minimum-cost flow problem, one of the first network problems with a polynomial-time ("good") algorithm in the sense of Edmonds.

Timeline. Hitchcock (1941) posed the problem; Ford and Fulkerson (1956–1962) gave the primal–dual labeling method and the optimality conditions by node potentials; Edmonds and Karp (1972) gave the scaling method and the bound formalized here. Strongly polynomial algorithms, independent of the size of the numbers, came later (Tardos 1985; Orlin 1988).

Setting

The network of Figure 1 (p. 259) has a source $s$ , a sink $t$ , supply nodes $s_1,\dots,s_m$ and demand nodes $t_1,\dots,t_n$ , with $m,n\ge 1$ . Its arcs are $(s,s_i)$ with capacity $a_i$ and cost $0$ ; $(s_i,t_j)$ with capacity $+\infty$ and cost $d_{ij}\ge 0$ ; $(t_j,t)$ with capacity $b_j$ and cost $0$ ; and the return arc $(t,s)$ with capacity $+\infty$ and cost $0$ . The supplies $a_i$ and demands $b_j$ are positive integers with $\sum_i a_i=\sum_j b_j=:B$ .

A flow assigns a nonnegative number to every arc, at most the capacity, with inflow equal to outflow at every node. Write $f_{0i}=f(s,s_i)$ , $f_{ij}=f(s_i,t_j)$ , $f_{j0}=f(t_j,t)$ ; the value of $f$ is $f(t,s)$ , and a maximum flow is one of largest value. Its cost is $\sum_{i,j} d_{ij} f_{ij}$ ; a flow is extreme if no flow of the same value is cheaper. A flow is pseudo-extreme if there are real $u_i, v_j$ with $u_i-v_j+d_{ij}\ge 0$ for all $i,j$ and $f_{ij}=0$ whenever $u_i-v_j+d_{ij}>0$ .

An augmenting path relative to $f$ is a sequence of distinct nodes from $s$ to $t$ in which each step either follows an arc with spare capacity or traverses backwards an arc carrying positive flow; augmenting pushes the minimum spare amount $\varepsilon$ along it and raises $f(t,s)$ by $\varepsilon$ .

For $p\ge 0$ , Problem $p$ has the same network and costs, with capacities $\lfloor a_i/2^p\rfloor$ and $\lfloor b_j/2^p\rfloor$ . Choose $l$ with every $a_i,b_j<2^l$ . The scaling method solves Problems $l-1,l-2,\dots,0$ in turn. Each phase performs augmentations keeping every flow pseudo-extreme, until no augmenting path is left. Problem $l-1$ starts from the zero flow, and Problem $p-1$ starts from twice the final flow of Problem $p$ .

Formalization targets

Goal: Theorem 9

For every run of the scaling method, the total number $\sum_{p<l} K_p$ of flow augmentations satisfies

\sum_{p=0}^{l-1} K_p \;\le\; \max(m,n)\left(2+\left\lfloor \log_2\frac{\sum_{i=1}^m a_i}{\max(m,n)}\right\rfloor\right).

The bound holds for every $l$ admissible for the data and every choice of costs, and is stated with the paper's constant exactly.

Milestones

§1.1: augmentation preserves feasibility and raises the value by $\varepsilon>0$ ; a flow is maximum iff no augmenting path exists.
Theorem 8: a maximum flow is extreme iff there are potentials $u_0,\dots,u_m$ , $v_0,\dots,v_n$ with (5a)–(5f).
§2.2: a pseudo-extreme maximum flow is extreme.
Lemma 3: if $f$ is pseudo-extreme in Problem $p$ , then $2f$ is pseudo-extreme in Problem $p-1$ .
The maximum-flow value of Problem $p$ is $f_p^*=\min\big(\sum_i\lfloor a_i/2^p\rfloor,\sum_j\lfloor b_j/2^p\rfloor\big)$ .
Eq. (6): $\sum_p K_p\le f_0^*-\sum_{p=1}^{l-1} f_p^*$ .
$f_p^*\ge\max\big(0,\,B/2^p-\max(m,n)\big)$ .

Significance

The result. Theorem 9 shows that scaling reduces the number of augmentations from order $B$ to order $\max(m,n)\log_2(B/\max(m,n))$ , which is roughly the length of the binary encoding of the data. Combined with the $O(mn)$ cost of one augmentation it gives a polynomial-time algorithm for the transportation problem; through the reduction of minimum-cost flow to transportation (p. 261) it gives one for minimum-cost flow. Capacity and cost scaling became standard techniques in network optimization and in combinatorial optimization generally. Theorem 8 and the pseudo-extreme criterion are the optimality certificates for transportation, a special case of linear-programming complementary slackness.

Formalizing it. The theorem has been proved since 1972. This mission produces a machine-checked version of the bound, of the exact counting argument (eq. (6)) and of the arithmetic estimate that turns it into the stated constant, together with the potential-based optimality conditions for the transportation network. To our knowledge no machine-checked bound on the number of augmentations of a flow algorithm exists on the platform.

Difficulty

The obvious argument bounds the number of augmentations by the increase in flow value, since each augmentation raises the value by a positive integer. Applied to Problem 0 directly this gives only $B$ . The scaling bound needs three things that the naive count does not supply. First, doubling the final flow of Problem $p$ must give a feasible, still pseudo-extreme, starting flow for Problem $p-1$ (Lemma 3). Second, the gap between that start and the optimum of Problem $p-1$ must be small, which requires the exact maximum-flow value $f_p^*$ of each scaled problem. Third, the telescoping sum of the gaps must be estimated against $\log_2(B/\max(m,n))$ with the floors handled exactly. Integrality of every intermediate flow is not assumed; it has to be carried along the run from the integral capacities and the zero start.

Formalization scope

Everything lives in the namespace EdmondsKarp.Scaling. Nodes form an inductive type (s, t, src i, dst j). A flow is a structure with components f0, fx, fz, ret for the four arc families, real valued; the infinite capacities are encoded by the absence of an upper bound. IsMaxFlow is a predicate comparing values with every flow, not a supremum. Problem $p$ uses natural-number division for $\lfloor a_i/2^p\rfloor$ . Augmenting paths are lists of distinct nodes from s to t whose consecutive pairs have positive residual amount (resCap, valued in WithTop ℝ); they never use the return arc.

A run of the scaling method (IsScalingRun) is a family of phases $F\,p\,0,\dots,F\,p\,(K\,p)$ for $p<l$ . It starts from $0$ in Problem $l-1$ , restarts from $2F\,p\,(K\,p)$ in Problem $p-1$ , and advances by one augmentation per step. Every flow is pseudo-extreme, and each phase ends with no augmenting path left. The paper's path-selection rule (minimum weight for the modified reduced costs $\bar\Delta$ ) is abstracted to this invariant, which the paper states for it, so every run of the paper's method is covered.

The goal compares the count, cast to $\mathbb{Z}$ , with $\max(m,n)\,(2+\lfloor\log_2(B/\max(m,n))\rfloor)$ , using Real.logb 2 and Int.floor. The constant is the printed one; neither $O(\cdot)$ nor a weaker constant is acceptable. Positivity of all $a_i,b_j$ is a hypothesis, because without it the printed bound is false (for $m=5$ , $n=1$ , $a=(1,0,0,0,0)$ , $b=(1)$ one augmentation is needed and the bound is negative). A formalization in which runs could be empty or never reach a maximum flow would trivialize the goal; the run predicate forbids this, and it is satisfiable (for instance with $m=n=1$ , $a=b=(1)$ , $l=1$ and one augmentation).

A complete development needs max-flow/min-cut for the bipartite network, integrality of flows along a run, the exact value of $f_p^*$ , the telescoping identity and floor/logarithm estimates. LP duality or complementary slackness is needed only for Theorem 8. The augmenting-path and max-flow lemmas are reusable for other bipartite flow problems. Contributions welcome: proofs of any milestone, and a formalization of the paper's exact $\bar\Delta$ path rule showing that it satisfies the invariant.

Selected references

J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5:247–255, 1985. https://doi.org/10.1007/BF02579369
J. B. Orlin, A faster strongly polynomial minimum cost flow algorithm, Proc. STOC 1988, 377–387. https://doi.org/10.1145/62212.62249

12 thms5 active usersReviewed

Captain: Lucas

Erdős Problem 77: the limit of R(k)^(1/k)Open Problem

Motivation

The diagonal Ramsey number $R(k)$ is the least $n$ such that every red/blue colouring of the edges of the complete graph $K_n$ contains a monochromatic copy of $K_k$ . Ramsey's theorem guarantees that $R(k)$ is finite; the question of how fast it grows is one of the central problems of extremal and probabilistic combinatorics. Erdős asked repeatedly ([Er88], [Er93]; see erdosproblems.com/77) for the value of

\lim_{k\to\infty} R(k)^{1/k}.

It is not even known whether this limit exists.

Timeline.

1935 — Erdős and Szekeres prove $R(k)\le\binom{2k-2}{k-1}$ , so $R(k)\le 4^{k}$ and $\limsup_k R(k)^{1/k}\le 4$ ([ES35]).
1947 — Erdős proves $R(k) > 2^{k/2}$ for $k\ge 3$ by a counting (probabilistic) argument, so $\liminf_k R(k)^{1/k}\ge\sqrt2$ ([Er47]).
1975 — Spencer improves the lower bound by a factor of $2$ : $R(k)\ge(1+o(1))\frac{\sqrt2}{e}\,k\,2^{k/2}$ ([Sp75]). The exponential base $\sqrt2$ has not been improved since.
2009, 2023 — Conlon ([Co09]) and then Sah ([Sa23]) obtain super-polynomial savings over $4^k$ , but still with exponential base $4$ .
2023 — Campos, Griffiths, Morris and Sahasrabudhe prove $R(k)\le(4-\varepsilon)^k$ for some constant $\varepsilon>0$ and all large $k$ : the first exponential improvement on the upper bound ([CGMS23]).
2024 — Gupta, Ndiaye, Norin and Wei optimise the CGMS method and obtain $R(k)\le 3.8^{k+o(k)}$ ([GNNW24]). Balister et al. extend exponential improvements to the multicolour setting ([BBCGHMST24]).

So today, if the limit exists, it lies in $[\sqrt2,\,3.8]$ .

Setting

For $n\in\mathbb N$ consider simple graphs $G$ on the vertex set $\{0,\dots,n-1\}$ . A red/blue colouring of the edges of $K_n$ is the same as such a graph $G$ (the red edges) together with its complement $G^{c}$ (the blue edges). A $k$ -clique of $G$ is a set of exactly $k$ vertices, any two of which are adjacent in $G$ . Define

R(k)=\min\bigl\{\,n\in\mathbb N:\ \text{every graph } G \text{ on } n \text{ vertices has a } k\text{-clique in } G \text{ or in } G^{c}\,\bigr\}.

In the Lean development this is Erdos77.diagonalRamsey k. Small values: $R(0)=0$ , $R(1)=1$ , $R(2)=2$ , $R(3)=6$ , $R(4)=18$ .

Formalization targets

Goal: existence of the limit

\exists\,L\in\mathbb R:\qquad R(k)^{1/k}\ \longrightarrow\ L\qquad (k\to\infty).

The original problem asks for the value of the limit, which is unknown; a goal with a hard-coded value cannot be stated honestly. The goal therefore asserts only that the limit exists (as a real number). Determining $L$ remains the ultimate aim; any proof of a specific value would in particular prove this goal.

Milestones (results from the literature)

Erdős 1947: $R(k)>2^{k/2}$ for all $k\ge 3$ .
Spencer 1975: for every $\varepsilon>0$ , eventually $R(k)\ge(1-\varepsilon)\frac{\sqrt2}{e}\,k\,2^{k/2}$ .
Erdős–Szekeres 1935: $R(k)\le\binom{2k-2}{k-1}$ for all $k\ge1$ .
Campos–Griffiths–Morris–Sahasrabudhe 2023: there is $\varepsilon>0$ with $R(k)\le(4-\varepsilon)^k$ for all sufficiently large $k$ .
Gupta–Ndiaye–Norin–Wei 2024: for every $\delta>0$ , eventually $R(k)\le 3.8^{(1+\delta)k}$ , i.e. $R(k)\le 3.8^{k+o(k)}$ .

Significance

The result itself. Existence of the limit would say that diagonal Ramsey numbers have a well-defined exponential growth rate — a regularity statement that is currently unknown in either direction. Even the bounds $\sqrt2\le\liminf$ and $\limsup\le 3.8$ are the products of decades of work, and the lower bound base $\sqrt2$ has resisted improvement since 1947.

Formalizing it. The goal is open. The milestones are proved results in the literature; the classical ones (Erdős–Szekeres, Erdős 1947) are natural first formalization targets, and the recent upper bounds (CGMS, GNNW) are substantial formalization projects in their own right. The status of existing machine-checked formalizations of these results is not asserted here.

Difficulty

There is no known sub- or super-multiplicativity for $R(k)$ that would give existence of the limit via Fekete's lemma: the natural product constructions relate $R(k\ell)$ to $R(k)$ and $R(\ell)$ only with losses that are too large, and the best lower and upper bounds come from entirely different methods (random colourings versus the book algorithm), so neither side controls the other.

Formalization scope

$R(k)$ is defined as an infimum over $n$ of the property "every graph on $\mathrm{Fin}\,n$ has a $k$ -clique in $G$ or in $G^{c}$ ". Lean's sInf of an empty set of naturals is $0$ ; the Erdős–Szekeres milestone shows the set is nonempty, so the infimum is the genuine Ramsey number.
$R(k)^{1/k}$ is the real power of the real number $R(k)$ with exponent $1/k$ ; the value at $k=0$ is irrelevant for the limit.
The limit is required to be a real number $L$ ; given the known bounds this loses nothing.
Asymptotic statements ("for all sufficiently large $k$ ") are expressed with the atTop filter on $\mathbb N$ ; " $o(k)$ " in GNNW is encoded as "for every $\delta>0$ , eventually with exponent $(1+\delta)k$ ".
Needed infrastructure: basic Ramsey theory for graphs on Fin n, binomial estimates, the probabilistic method for the lower bounds (Spencer uses the Lovász Local Lemma), and the CGMS book algorithm for the upper bounds. All of these are reusable beyond this mission.

Selected references

[Er47] P. Erdős, Some remarks on the theory of graphs, Bull. Amer. Math. Soc. 53 (1947), 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-1
[ES35] P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Math. 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/
[Sp75] J. Spencer, Ramsey's theorem — a new lower bound, J. Combin. Theory Ser. A 18 (1975), 108–115. https://doi.org/10.1016/0097-3165(75)90071-0
[Co09] D. Conlon, A new upper bound for diagonal Ramsey numbers, Ann. of Math. 170 (2009), 941–960. https://doi.org/10.4007/annals.2009.170.941
[Sa23] A. Sah, Diagonal Ramsey via effective quasirandomness, Duke Math. J. 172 (2023). https://arxiv.org/abs/2005.09251
[CGMS23] M. Campos, S. Griffiths, R. Morris, J. Sahasrabudhe, An exponential improvement for diagonal Ramsey, arXiv:2303.09521 (2023). https://arxiv.org/abs/2303.09521
[GNNW24] P. Gupta, N. Ndiaye, S. Norin, L. Wei, Optimizing the CGMS upper bound on Ramsey numbers, arXiv:2407.19026 (2024). https://arxiv.org/abs/2407.19026
[BBCGHMST24] P. Balister, B. Bollobás, M. Campos, S. Griffiths, E. Hurley, R. Morris, J. Sahasrabudhe, M. Tiba, Upper bounds for multicolour Ramsey numbers, arXiv:2410.17197 (2024). https://arxiv.org/abs/2410.17197
[Er88] P. Erdős, Problems and results in combinatorial analysis and graph theory, Discrete Math. 72 (1988), 81–92.
[Er93] P. Erdős, Some of my favorite solved and unsolved problems in graph theory, Quaestiones Math. 16 (1993), 333–350.
Erdős Problems, Problem #77. https://www.erdosproblems.com/77

66 thms5 active usersReviewed

Captain: Lucas

Erdős Problem 20: The Sunflower ConjectureOpen Problem

Motivation

A sunflower (also called a $\Delta$ -system) with $k$ petals is a family of $k$ sets whose pairwise intersections are all equal to one common set, the kernel. In 1960 Erdős and Rado proved the sunflower lemma: every sufficiently large family of $n$ -element sets contains a sunflower with $k$ petals, and they asked how large "sufficiently large" must be (Erdős–Rado 1960). The conjecture that the threshold is only exponential in $n$ is one of Erdős' best-known problems in extremal combinatorics; it is listed as Erdős Problem 20, and Erdős offered a $1000 prize for it. Sunflower bounds are used, for example, in Razborov's monotone circuit lower bounds and in the study of set systems with restricted intersections.

Timeline.

1960 — Erdős and Rado prove $(k-1)^n < f(n,k) \le (k-1)^n\, n! + 1$ and conjecture $f(n,k) \le c_k^{\,n}$ (ErRa60).
2019 — Alweiss, Lovett, Wu and Zhang prove $f(n,k) \le (C k^3 \log n \log\log n)^n$ , the first bound of the form $(\log n)^{n(1+o(1))}$ for fixed $k$ (arXiv:1908.08483).
2020 — Rao simplifies the argument via Shannon's noiseless coding theorem and obtains $(\alpha k \log(kn))^n$ (arXiv:1909.04774); Tao gives an entropy proof of the same bound.
2021 — Bell, Chueluecha and Warnke obtain $f(n,k) \le (C k \log n)^n$ for $n,k \ge 2$ (arXiv:2009.09327).

The conjecture itself remains open, even for $k = 3$ .

Setting

Fix natural numbers $n$ (the uniformity) and $k$ (the number of petals). A family $\mathcal F$ of sets is $n$ -uniform if every member of $\mathcal F$ has exactly $n$ elements. A subfamily $\mathcal S \subseteq \mathcal F$ is a $k$ -sunflower if $|\mathcal S| = k$ and there is a set $Y$ with $A \cap B = Y$ for all distinct $A, B \in \mathcal S$ .

The sunflower threshold $f(n,k)$ is the least natural number $m$ such that every $n$ -uniform family $\mathcal F$ (over any ground set) with $|\mathcal F| \ge m$ contains a $k$ -sunflower.

Formalization targets

Goal — the sunflower conjecture (Erdős Problem 20)

\exists\, c:\mathbb N\to\mathbb N\quad \forall n \ge 1,\ \forall k:\qquad f(n,k) < c_k^{\,n}.

The constants $c_k$ are left unspecified; only the exponential shape in $n$ is asked for. A disproof (the negation of this statement) would equally settle the problem.

Milestones from the literature

Erdős–Rado upper bound: $f(n,k) \le (k-1)^n\, n! + 1$ for $n \ge 1$ , $k \ge 2$ .
Erdős–Rado lower bound: $(k-1)^n < f(n,k)$ for $n \ge 1$ , $k \ge 2$ .
Rao's bound: there is $\alpha > 1$ with $f(n,k) \le (\alpha k \log(kn))^n + 1$ for $n \ge 1$ , $k \ge 2$ .
Bell–Chueluecha–Warnke bound: there is $C \ge 4$ with $f(n,k) \le (C k \log n)^n$ for $n, k \ge 2$ .

A supporting sanity check, $f(0,1) = 1$ , is taken from the source formalization.

Significance

A positive answer would show that sunflower-free $n$ -uniform families have at most exponential size, the correct order of magnitude by the Erdős–Rado lower bound; this would sharpen every application that currently loses a $\log n$ factor per coordinate, including monotone circuit lower bounds. A negative answer would show the $(\log n)^n$ -type bounds of 2019–2021 are essentially the truth.

On the formal side, the Erdős–Rado upper bound has a Lean formalization recorded in the source file; the lower-bound construction and the spread-family / coding arguments behind the Rao and Bell–Chueluecha–Warnke bounds are, as far as this proposal records, not yet formalized. Formalizing them produces reusable infrastructure on spread families and random-subset (or entropy) arguments.

Difficulty

The classical induction on $n$ (pick a maximal family of pairwise disjoint members; if it is small, some element lies in many members, recurse on the link) loses a factor of about $n$ at each of $n$ steps, which is where $n!$ comes from. The modern arguments replace the recursion by an analysis of spread families, but each still loses a factor $\log n$ per level, and no known technique removes it. The case $k = 3$ is already open.

Formalization scope

The ground set is an arbitrary type in the lowest universe; set families are Set (Set α) and sizes are measured with Set.ncard, which returns $0$ on infinite sets. Consequently, for $n \ge 1$ only finite members can be " $n$ -element", and the condition $m \le |\mathcal F|$ with $m \ge 1$ only applies to finite families. All targets assume $n \ge 1$ (except the sanity check), so the $n = 0$ quirks do not affect them.
$f(n,k)$ is defined as an infimum over natural numbers; if no admissible $m$ existed the infimum would be $0$ . The Erdős–Rado upper bound shows the admissible set is non-empty for $n \ge 1$ .
Logarithms are natural logarithms; changing the base only rescales the unspecified constants.
The goal is stated as the positive claim of the conjecture, not as a yes/no answer(·) statement.

Contributions of general lemmas on sunflowers, spread families and the Erdős–Rado construction are welcome and reusable beyond this mission.

Selected references

P. Erdős, R. Rado, Intersection theorems for systems of sets, J. London Math. Soc. 35 (1960), 85–90. doi:10.1112/jlms/s1-35.1.85
R. Alweiss, S. Lovett, K. Wu, J. Zhang, Improved bounds for the sunflower lemma, Annals of Mathematics 194 (2021). arXiv:1908.08483
A. Rao, Coding for sunflowers, Discrete Analysis 2020:2. arXiv:1909.04774
T. Bell, S. Chueluecha, L. Warnke, Note on sunflowers, Discrete Mathematics 344 (2021). arXiv:2009.09327
Erdős Problem 20. erdosproblems.com/20

15 thms5 active usersReviewed

Graph Theory·Captain: hao jia

P3-Partitions of Cubic 3-Connected Graphs (OPG-46613)Open Problem

Motivation

A $P_3$ -packing in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.

A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of Packing 3-vertex Paths in Cubic 3-connected Graphs, the question is whether every cubic 3-connected graph $G$ satisfies $\lambda(G)=\lfloor |V(G)|/3\rfloor$ . Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. OPG-46613 records the divisible-order form targeted here.

A 2026 candidate analysis in the Vibe Mathing problem repository investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a $P_3$ -factor. Candidate C02 gives an explicit proposed family $H_q$ of order $18+12q$ that has $P_3$ -factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.

Setting

All graphs are finite and simple. A graph is cubic when every vertex has exactly three neighbors. It is 3-vertex-connected here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.

A $P_3$ -factor is represented by a natural number $b$ , together with a bijection

\operatorname{Fin}(b)\times\operatorname{Fin}(3)\simeq V(G),

such that, in every block, positions $0$ and $1$ are adjacent and positions $1$ and $2$ are adjacent. The path is not required to be induced: an ambient edge between positions $0$ and $2$ is allowed because the two selected path edges still form a copy of $P_3$ .

A 2-factor is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A divisible matching complement is a perfect matching $M$ such that the relative complement $G\setminus M$ is a divisible 2-factor.

The explicit graph $H_q$ is defined on $\operatorname{Fin}(18+12q)$ . Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.

Formalization targets

Main goal

For every finite simple graph $G$ ,

\bigl(G\text{ cubic}\bigr)\land \bigl(G\text{ 3-vertex-connected}\bigr)\land 3\mid |V(G)| \quad\Longrightarrow\quad G\text{ has a }P_3\text{-factor}.

This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.

Literature and route milestones

The mission also formalizes the $(z1)\Leftrightarrow(z8)$ part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a $P_3$ -factor. Two route lemmas state that divisible 2-factors split into $P_3$ -factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.

Candidate boundary milestones

The C02 milestones ask first for the complete 18-vertex statement and then for the full family:

\forall q\in\mathbb N,\quad H_q\text{ is cubic and 3-vertex-connected, has a }P_3\text{-factor, and has no divisible matching complement}.

This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every $H_q$ in the proposed family explicitly satisfies the desired $P_3$ conclusion.

Significance

A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a $P_3$ -factor; the C02 family does not claim this.

Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced $P_3$ -factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.

Difficulty

The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated $P_3$ -factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.

The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to $G$ on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and $P_3$ must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.

Formalization scope

The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Graphs use SimpleGraph on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.

The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The $H_q$ family includes $q=0$ . The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in sorry; the shared definition module itself is sorry-free.

Welcome contributions include proofs of the model lemmas, the finite $H_0$ statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.

Selected references

A. Kelmans, Packing 3-vertex Paths In Cubic 3-connected Graphs, arXiv:0910.2766v2, 2011, Problem 1.10 (p. 3) and Theorem 3.1 (pp. 7–8). https://arxiv.org/abs/0910.2766v2
UnsolvedMath, OPG-46613: P3-partitions of cubic 3-connected graphs. https://www.unsolvedmath.com/problems/OPG-46613
Vibe Mathing, C01: divisible-cycle implication and a 30-vertex obstruction, fixed repository revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md
Vibe Mathing, C02: an 18-vertex obstruction and an infinite family with P3-factors, fixed repository revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.md

16 thms5 active usersReviewed

Linear Optimization·Captain: Shuze Chen

The Polynomial Hirsch ConjectureOpen Problem

Motivation

The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$ -dimensional polytope with $n$ facets is at most $n - d$ . Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the polynomial Hirsch conjecture: is the diameter bounded by a polynomial in $n$ and $d$ ?

Timeline

1957. Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in Linear Programming and Extensions (1963).
1964–1966. Klee determines the exact maximum diameter of $3$ -polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three.
1967. Klee and Walkup (Acta Math.) refute the unbounded-polyhedron version, prove the bounded conjecture for $n - d \le 5$ , and reduce the general case to the $d$ -step conjecture ( $n = 2d$ ).
1970. Larman (Proc. LMS) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape.
1989. Naddef (Math. Programming) proves $0/1$ -polytopes satisfy the Hirsch bound, with diameter at most $d$ .
1992. Kalai and Kleitman (Bull. AMS) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart.
2010. Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches Polymath 3 on the polynomial version.
2010–2012. Santos (Annals of Math.) disproves the Hirsch conjecture: a $43$ -dimensional polytope with $86$ facets and diameter at least $44$ , via spindles of large width.
2014–2019. Todd (SIAM J. Discrete Math.) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$ ; Sukegawa refines further. Matschke, Santos, and Weibel (Proc. LMS 2015) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$ . All known violations remain constant-factor; all known bounds remain quasi-polynomial.

Setting

Work in $\mathbb{R}^d$ . An H-polytope is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$ , it is

P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},

where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$ . Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts.

A vertex of $P$ is an extreme point. Two vertices $u \ne v$ are adjacent when the segment $[u, v]$ is an extreme subset of $P$ ; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an edge. The combinatorial diameter of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$ " is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim.

Formalization targets

Goal — the polynomial Hirsch conjecture

\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.

Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.

Milestones — the known ladder

Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$ ; Naddef's bound $d$ for $0/1$ -polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$ ; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$ ; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$ .

Significance

A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR 2010) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.

None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.

Difficulty

The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving any polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters large is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.

Formalization scope

The Lean model commits to: ambient space EuclideanSpace ℝ (Fin d); the polytope as Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i} for a : Fin n → EuclideanSpace ℝ (Fin d), b : Fin n → ℝ, with nonemptiness and Bornology.IsBounded as explicit hypotheses (boundedness is essential: Klee–Walkup's unbounded counterexample would otherwise trivialize the Santos milestone); vertices as Set.extremePoints ℝ; adjacency as u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v); and diameter bounds as the walk predicate DiamLE, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through Real.logb and the natural floor. In larman_bound and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with todd_bound requiring full-dimensionality ((interior P).Nonempty) as in its source.

Welcome contributions: any milestone in any order (dimension_three_bound for $d \le 1$ cases and structural lemmas about Adj and DiamLE are natural entry points, and kalai_kleitman_bound is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.

Selected references

V. Klee, D. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967). doi:10.1007/BF02392971
D. Larman, Paths on polytopes, Proc. London Math. Soc. 20 (1970). doi:10.1112/plms/s3-20.2.249
D. Naddef, The Hirsch conjecture is true for (0,1)-polytopes, Math. Programming 45 (1989). doi:10.1007/BF01589418
G. Kalai, D. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. AMS 26 (1992). arXiv:math/9204233
F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176 (2012). arXiv:1006.2814
M. Todd, An improved Kalai–Kleitman bound for the diameter of a polyhedron, SIAM J. Discrete Math. 28 (2014). arXiv:1402.3579
B. Matschke, F. Santos, C. Weibel, The width of five-dimensional prismatoids, Proc. London Math. Soc. 110 (2015). arXiv:1202.4701
F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of polyhedra: limits of abstraction, Math. Oper. Res. 35 (2010). doi:10.1287/moor.1100.0470
F. Santos, Recent progress on the combinatorial diameter of polytopes and simplicial complexes, TOP 21 (2013) (survey). arXiv:1307.5900

81 thms5 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior IX: Solutions for Acyclic RelationsTextbook

Motivation

The solution concept of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944) is defined from two ingredients: a set of imputations and a domination relation between them. A solution is a set of imputations that is internally stable (no member dominates another) and externally stable (every non-member is dominated by some member). In §65 of the book the authors observe that this definition never uses what imputations and domination actually are. They abstract it to an arbitrary set $D$ and an arbitrary relation $\mathcal S$ on $D$ , and ask which properties of $\mathcal S$ guarantee that exactly one solution exists.

The abstract notion is what graph theory now calls a kernel of a directed graph: draw an arc $x \to y$ whenever $x\mathcal S y$ ; a solution is a set of vertices that is independent and absorbs every vertex outside it. Kernels appear in combinatorial game theory (the losing positions of a finite impartial game form a kernel of its move graph) and in the theory of preference and choice.

Timeline.

1944 (1st ed.; 3rd ed. 1953, reprinted 2007): von Neumann and Morgenstern define solutions for an arbitrary relation (§65), show that a finite set with an acyclic relation has exactly one solution (65:X), and that acyclicity is necessary for every subset to have a unique solution (65:Z).
1953: M. Richardson, Solutions of irreflexive relations, extends existence (not uniqueness) to finite relations without cycles of odd length.

Setting

Let $D$ be an arbitrary set and $\mathcal S$ an arbitrary relation on $D$ ; $x\mathcal S y$ is read " $x$ dominates $y$ ". A solution (in $D$ for $\mathcal S$ ) is a set $V \subseteq D$ with

\text{(65:1)}\qquad V = \{\, y \in D : x\mathcal S y \text{ holds for no } x \in V \,\}.

For $E \subseteq D$ , an element $x$ is a maximum of $E$ if $x \in E$ and no $y \in E$ has $y\mathcal S x$ ; the set of maxima is $E^m$ .

For $m \ge 1$ , condition $(A_m)$ says: never $x_1\mathcal S x_0, x_2\mathcal S x_1, \dots, x_m\mathcal S x_{m-1}$ with $x_0 = x_m$ and all $x_i \in D$ . The relation is acyclic if it satisfies every $(A_m)$ , $m = 1, 2, \dots$ ; in particular never $x\mathcal S x$ . It is strictly acyclic if there is no infinite sequence $x_0, x_1, x_2, \dots$ in $D$ with $x_{i+1}\mathcal S x_i$ for every $i$ . Property (65:K) says that every non-empty $E \subseteq D$ has $E^m \ne \ominus$ . A partial ordering (65:B) is a transitive relation for which at most one of $x = y$ , $x\mathcal S y$ , $y\mathcal S x$ holds.

For the main theorem the book constructs a candidate solution by induction (65.7.1): $A_1 = D$ ; $B_i = A_i^m$ ; $C_i$ is the set of elements of $A_i$ dominated by some element of $B_i$ ; $A_{i+1} = A_i - B_i - C_i$ . With $i_0$ the first index for which $A_{i_0} = \ominus$ ,

\text{(65:2)}\qquad V_0 = B_1 \cup \cdots \cup B_{i_0 - 1}.

In Lean the elements live in a type α, D V : Set α, and S : α → α → Prop with S x y meaning $x\mathcal S y$ ; the predicates are IsSolution D S V, maxima E S, IsAcyclic, IsStrictlyAcyclic, HasMaximaProperty, IsPartialOrdering, ConditionG, and the construction stageA, stageB, stageC, V0.

Formalization targets

Goal: (65:X)

If $D$ is finite and $\mathcal S$ is acyclic on $D$ , then

\exists!\, V:\ V \text{ is a solution in } D \text{ for } \mathcal S, \qquad\text{and}\qquad V \text{ is a solution} \iff V = V_0 .

Milestones, in attack order

(65:I) For a partial ordering, a finite $D$ satisfies (65:G): every non-maximal $y$ is dominated by some maximum.
(65:H) For a partial ordering of an arbitrary $D$ : $V$ is a solution $\iff$ (65:G) holds and $V = D^m$ .
(65:O:c) Strict acyclicity implies acyclicity; for finite $D$ the two are equivalent.
(65:P) (65:K) $\iff$ strict acyclicity, for arbitrary $D$ .
(65:S) For finite $D$ and acyclic $\mathcal S$ , some $A_i$ is empty.
(65:V) For finite $D$ and acyclic $\mathcal S$ , every solution equals $V_0$ .
(65:W) For finite $D$ and acyclic $\mathcal S$ , $V_0$ is a solution.
(65:Z) If every $E \subseteq D$ has a unique solution in $E$ for $\mathcal S$ , then $\mathcal S$ is acyclic on $D$ .

Significance

The result itself. (65:X) is the most general of the book's three existence-and-uniqueness theorems for solutions (complete ordering, partial ordering, acyclic relation; 65.8.1). For games proper it has no direct application: the set of imputations of an essential game has no maxima, so (65:K) fails (65.9.1). Its role is to isolate a sufficient condition for a unique solution. With (65:Z), and applied to every subset of $D$ , it characterizes the finite relations for which every subset has exactly one solution: exactly the acyclic ones (65.8.2). In graph language it is the statement that a finite directed acyclic graph has exactly one kernel. In combinatorial game theory this is the partition of the positions of a finite impartial game into P- and N-positions. The complete- and partial-ordering results (65:E)–(65:I) are the special cases the book treats first.

Formalizing it. The results are classical and fully proved in the book; to the best of our knowledge none of them is on the Prove2Me platform, and Mathlib has well-foundedness (WellFounded, RelEmbedding of ℕ) but no kernel or von Neumann–Morgenstern solution notion for an abstract relation. The mission produces machine-checked proofs of the book's §65 chain: the equivalence of (65:K) with strict acyclicity for arbitrary sets, the finite equivalence of acyclicity and strict acyclicity, the explicit construction of $V_0$ , and the characterization of 65.8.2.

Difficulty

Most of the individual steps are short. The work is in making the book's finite induction precise. The sets $A_i$ are defined recursively and $V_0$ refers to the first empty stage $i_0$ . The uniqueness proof (65:V) is a minimal-counterexample argument over the stage index, which moves between "smallest $k$ with $y \notin A_k$ " and the disjoint decomposition (65:U) of $D$ into the $B_i$ and $C_i$ . A tempting shortcut, taking an arbitrary well-founded rank function instead of the book's construction, proves existence and uniqueness but not that the solution is the $V_0$ of (65:2), which is part of the goal. For (65:P) and (65:O:c) the difficulty is the passage between finite cycles and infinite chains. Going from a chain in a finite set to a repetition needs a pigeonhole argument, and going from a set without maxima to a chain needs dependent choice.

Formalization scope

Representation. An ambient type α; D, E, V are Set α; the relation is S : α → α → Prop and is only ever consulted on elements of the set under consideration, so it is the book's relation on $D$ (or its restriction to $E$ ). Finite and infinite sequences are functions ℕ → α.
Solutions. IsSolution D S V is the set equation (65:1) literally; it forces $V \subseteq D$ . Uniqueness in the goal is ∃! over all V : Set α, not over a subtype; there is no degenerate reading in which the solution is fixed by construction.
Acyclicity. IsAcyclic D S requires $(A_m)$ for every $m \ge 1$ , all cycle elements in $D$ . The case $m = 0$ is excluded, as in the book (it would be unsatisfiable). This is equivalent to the absence of a Relation.TransGen loop inside $D$ , but the book's form is stated.
Construction. Stages are indexed from $0$ : stageA D S k is the book's $A_{k+1}$ . V0 D S is the union of all $B_i$ , which equals $B_1 \cup \cdots \cup B_{i_0 - 1}$ because every later $B_i$ is empty.
Standing hypotheses instantiated. (65:S), (65:V), (65:W) and the goal (65:X) carry the hypotheses of 65.7.1, " $D$ finite and $\mathcal S$ acyclic" (for finite $D$ equivalently strictly acyclic, i.e. (65:K)), as D.Finite and IsAcyclic D S. (65:H) and (65:I) carry the partial-ordering hypothesis (65:B:a), (65:B:b) of 65.5.1, and (65:I) also finiteness of $D$ . (65:O:c), (65:P) and (65:Z) are for arbitrary $D$ and $\mathcal S$ , as 65.6.2 and 65.8.2 state. The empty $D$ is allowed everywhere; there the unique solution is $\ominus$ .
Not stated. The infinite case of (65:X) and of (65:Y), which the book leaves open (65.7.1, 65.8.3, question (65:9)); the complete-ordering results (65:E), (65:F), which silently assume $D \neq \ominus$ ; the counting statement (65:8).
Needed infrastructure. Finite-set induction and pigeonhole on Set.Finite, dependent choice for (65:P). The definitions are reusable for any later work on kernels of digraphs and on abstract stable sets. Proofs of any milestone, and alternative proofs of the goal, are welcome.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §65, pp. 587–602. https://doi.org/10.1515/9781400829460
M. Richardson, Solutions of irreflexive relations, Annals of Mathematics 58 (1953), 573–590. https://doi.org/10.2307/1969755

13 thms4 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

The Distributionally Robust Chance-Constrained Vehicle Routing Problem I: With a Subadditive Demand Estimator the Two-Index Vehicle Flow Formulation Is ExactResearch Paper

Motivation

The capacitated vehicle routing problem (CVRP) asks for delivery routes of minimum cost. Each route starts and ends at a depot, every customer is visited exactly once, and the demand served on a route does not exceed the vehicle capacity. The problem is central in logistics and one of the most studied problems in combinatorial optimization. Its standard exact methods are branch-and-cut algorithms built on the two-index vehicle flow formulation, a 0/1 program over arcs whose capacity constraints are the rounded capacity inequalities (RCIs); see Laporte, Nobert and Desrochers (1985) and Semet, Toth and Vigo (2014).

In practice customer demands are uncertain. A chance-constrained CVRP requires each route to respect its capacity with probability at least $1-\epsilon$ under a known distribution. That distribution is rarely known. Most solution methods also need independent demands. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP. There the chance constraint must hold for every distribution in an ambiguity set $\mathcal P$ of plausible distributions. The ambiguity set may contain dependent distributions and uncountably many of them, so it is not clear a priori that the problem can be solved by the usual branch-and-cut machinery. This mission formalizes the paper's answer to that question: its Theorem 1 and the counterexample that precedes it.

Setting

The graph is complete and directed. Its nodes are $V=\{0,\dots,n\}$ and its arcs are $A=\{(i,j)\in V\times V:i\neq j\}$ . Node $0$ is the depot and $V_C=\{1,\dots,n\}$ are the customers. There are $m$ vehicles, indexed by $K=\{1,\dots,m\}$ , each of capacity $Q>0$ . Traversing the arc $(i,j)$ costs $c(i,j)\ge 0$ ; costs may be asymmetric.

A route $\mathbf R_k=(R_{k,1},\dots,R_{k,n_k})$ is an ordered list of customers, with $R_{k,0}=R_{k,n_k+1}=0$ . A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)\in\mathfrak P(V_C,m)$ partitions $V_C$ into $m$ nonempty ordered routes. Its cost is $c(\mathbf R)=\sum_{k}\sum_{l=0}^{n_k}c(R_{k,l},R_{k,l+1})$ .

The demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ is random. The ambiguity set $\mathcal P$ is a set of probability distributions of $\tilde{\boldsymbol q}$ and $\epsilon\in(0,1)$ is the risk level. The problem RVRP( $\mathcal P$ ) minimizes $c(\mathbf R)$ over route sets such that

\mathbb P\Big[\textstyle\sum_{i\in\mathbf R_k}\tilde q_i\le Q\Big]\ge 1-\epsilon\qquad\forall\,\mathbb P\in\mathcal P,\ \forall\,k\in K .

With $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x:\mathbb Q[\tilde X\le x]\ge1-\epsilon\}$ , the demand estimator of the paper's Eq. (2) is

d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .

The problem 2VF( $\mathcal P$ ) minimizes $\sum_{(i,j)\in A}c(i,j)x_{ij}$ over $x\in\{0,1\}^A$ with in- and out-degree $1$ at every customer and $m$ at the depot, and with the RCIs

\sum_{i\in V\setminus S}\sum_{j\in S}x_{ij}\ge d_{\mathcal P}(S)\qquad\forall\,S\subseteq V_C,\ S\neq\emptyset .

A route set induces the arc vector with $x_{ij}=1$ exactly when $(i,j)=(R_{k,l},R_{k,l+1})$ for some $k,l$ (the paper's Eq. (3)). The estimator satisfies the subadditivity condition (S) if $d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)$ for all $S,T\subseteq V_C$ .

Formalization targets

Goal: Theorem 1

Assume $\tilde{\boldsymbol q}\ge\mathbf 0$ $\mathbb P$ -a.s. for all $\mathbb P\in\mathcal P$ , and assume $d_{\mathcal P}$ is real valued and satisfies (S). Then:

\begin{aligned} &\text{(i)}\ \ \mathbf R \text{ feasible in RVRP}(\mathcal P)\ \Longrightarrow\ x(\mathbf R)\text{ feasible in 2VF}(\mathcal P),\ \ c(x(\mathbf R))=c(\mathbf R);\\ &\text{(ii)}\ \ x\text{ feasible in 2VF}(\mathcal P)\ \Longrightarrow\ x=x(\mathbf R)\text{ for an RVRP}(\mathcal P)\text{-feasible }\mathbf R,\text{ unique up to reordering routes},\ c(x)=c(\mathbf R). \end{aligned}

Milestones

The chance constraint $\mathbb Q[\tilde X\le\tau]\ge1-\epsilon$ is equivalent to $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]\le\tau$ (p. 720).
Eq. (1): a route satisfies its robust chance constraint if and only if the worst-case VaR of its cumulative demand is at most $Q$ .
Example 1: an instance with two customers where a route set is RVRP( $\mathcal P$ )-feasible, yet its induced flow violates the RCI for $S=\{1,2\}$ , since $d_{\mathcal P}(\{1,2\})\ge3$ .
Example 1 (continued): on that instance $d_{\mathcal P}$ violates (S).
Theorem 1 (i) and 6. Theorem 1 (ii), stated separately.

Significance

Theorem 1 separates the modeling question from the algorithmic one. Whenever the ambiguity set yields a subadditive estimator, the distributionally robust CVRP is solved exactly by a two-index flow branch-and-cut. The only change from the deterministic case is the right-hand side $d_{\mathcal P}(S)$ of the RCIs, however many distributions $\mathcal P$ contains. The companion missions of this series show that (S) holds for every moment ambiguity set (Theorem 2 of the paper) and compute $d_{\mathcal P}$ for several classes of such sets. Example 1 shows that the hypothesis cannot be dropped: ambiguity sets that pin down each customer's marginal distribution break the equivalence.

The paper's proofs are in its online supplement; no machine-checked version of these statements exists. Formalizing them produces a checked reduction between a stochastic routing model and an integer program. It also produces reusable definitions of route sets, induced arc flows and RCIs over directed graphs with a depot.

Difficulty

Direction (ii) is a graph decomposition. A 0/1 vector with the prescribed degrees splits into $m$ depot cycles plus possibly depot-free subtours. The RCIs, through the $\max\{\cdot,1\}$ in $d_{\mathcal P}$ , must exclude the subtours, and the RCI on the customers of a single route must enforce that route's chance constraint. Uniqueness up to reordering requires that directed routes are recovered from arcs.

Direction (i) is where (S) enters. The naive argument bounds the number of vehicles entering $S$ by $d_{\mathcal P}(S)$ directly from the chance constraints. It fails because the chance constraints control each route separately, while $d_{\mathcal P}(S)$ looks at the joint worst case of the demands in $S$ ; Example 1 is exactly this failure. A set $S$ is typically visited by several routes, each covering only part of it. Relating the per-route guarantees to the joint quantity $d_{\mathcal P}(S)$ needs both hypotheses of the theorem: nonnegative demands and (S).

Formalization scope

Customers are Fin n (0-based; the paper's customer $i$ is i - 1). Nodes are Fin (n+1) with the depot 0 and customer i at i.succ, and vehicles are Fin m. A route set is R : Fin m → List (Fin n): every route is nonempty and the concatenated routes are a permutation of all customers. Arc vectors are ℕ-valued functions on ordered node pairs, with values in $\{0,1\}$ and the non-arcs $(i,i)$ fixed to $0$ .

Distributions are measures on Fin n → ℝ, and the ambiguity set is a set of probability measures. Chance constraints are written ENNReal.ofReal (1 - ε) ≤ P {q | …}. Value-at-risk is the published MultistageStochastic.valueAtRisk at level 1 - ε. The worst-case VaR is a real sSup and $d_{\mathcal P}$ is integer valued.

Two conventions implicit on the page are explicit hypotheses:

$Q>0$ , because (2) divides by $Q$ ;
boundedness of the VaR values for every customer set, which encodes the paper's declaration $d_{\mathcal P}:2^{V_C}\to\mathbb R_+$ .

A real sSup of an unbounded set is $0$ in Lean. Without the boundedness hypothesis every such estimator would silently equal $1$ and (ii) would fail. For an empty ambiguity set the Lean estimator equals $1$ on nonempty sets, as the paper's does.

The RCIs range over all nonempty customer sets with the depot on the outside. The estimator keeps the ceiling and the $\max\{\cdot,1\}$ . 2VF feasibility mentions neither routes nor chance constraints. RVRP feasibility does not mention $d_{\mathcal P}$ . A formalization in which either side refers to the other, or in which $d_{\mathcal P}$ drops the $\max\{\cdot,1\}$ , is not this theorem.

Useful contributions include lemmas on the decomposition of degree-constrained 0/1 arc vectors into depot cycles, monotonicity of VaR under almost-sure ordering, and the CDF right-continuity behind milestone 1.

Related platform work: SupplyChainTheory_vrp formalizes a different, symmetric, unit-demand VRP and is not reused.

Selected references

S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
G. Laporte, Y. Nobert, M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
F. Semet, P. Toth, D. Vigo, Classical exact algorithms for the capacitated vehicle routing problem, in P. Toth, D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014, 37–57. https://doi.org/10.1137/1.9781611973594.ch2
J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100(2):423–445, 2004. https://doi.org/10.1007/s10107-003-0481-8

12 thms4 active usersReviewed

Convex Optimization Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXII: Convex Extensibility of M-Convex FunctionsTextbook

Motivation

A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission 22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results on minimizer structure, gross substitutability, and convex extension that this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross substitutes and stepwise gross substitutes properties and their characterizing role, a minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this mission's goal — the theorem characterizing M-convexity entirely through the polyhedral structure of a function's convex extension.

Setting

Fix a finite ground set $V$ . For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain, write $f[p](x) = f(x) - \langle p,x \rangle$ for the linear reweighting by $p \in \mathbb R^V$ , and $\arg\min g = \{x : g(x) \le g(y)\ \forall y\}$ for the minimizer set of any function $g$ . The convex closure $\bar f(x)$ of $f$ at a real point $x$ is the infimum, over finite convex combinations of points of $\operatorname{dom} f$ representing $x$ , of the corresponding combination of function values; $f$ is convex extensible if $\bar f$ agrees with $f$ on $\mathbb Z^V$ , and integrally convex if $\bar f(x)$ can always be computed using only points from $x$ 's own integral neighborhood $N(x)$ (the integer vectors within one unit of $x$ in every coordinate). A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$ , some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold for every $\alpha \in [0,\alpha_0]$ .

Formalization targets

Goal: convex extensibility characterizes M-convexity

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain,

f \text{ is M-convex} \iff \bigl(f \text{ is convex extensible}\bigr) \wedge \bigl(\forall p \in \mathbb R^V,\ \arg\min \bar f[-p] \text{ is an M-convex polyhedron, if nonempty}\bigr),

with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.

Supporting structural targets

Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).

Significance

Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.

None of these results are open — they are Murota's systematic account of a theory with roots in matroid theory, submodular optimization, and mathematical economics. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.43 (M-convex $\implies$ convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron $B = \arg\min f$ : every edge of an M-convex polyhedron must be parallel to some $\chi_u - \chi_v$ , a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ (integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex closure is built directly from finite convex-combination representations rather than an abstract closure operator, and integral convexity compares it against the same construction restricted to each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets, reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45, 6.47) are formalized from the book's primal (interval-of- $\alpha$ ) definition, not the directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is correspondingly stated with only its first two legs (see Difficulty and MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing omission, since the six results using the primal axiom already exercise the chapter's real- variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.44's shared-coefficient construction carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
A. S. Kelso Jr. and V. P. Crawford, "Job matching, coalition formation, and gross substitutes," Econometrica, 50 (1982), pp. 1483-1504.
F. Gul and E. Stacchetti, "Walrasian equilibrium with gross substitutes," Journal of Economic Theory, 87 (1999), pp. 95-124.

47 thms4 active usersReviewed

Combinatorics

Missions

Proofs from THE BOOKTextbook

Proofs from THE BOOK: verified results and open formalization tasks

What is already verified

Sixth-edition contribution targets

Chapter numbering and statement scope

How to contribute

Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem

1. Motivation

2. Setting

3. Target

4. Significance

5. Difficulty

6. Formalization scope

7. Selected references

Scheduling Subject to Resource Constraints: Classification and Complexity II: Unit-Time Jobs on Two Uniform Machines with Unit Resources Are Strongly NP-hardResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Convexity and Steinitz's Exchange Property III: Fenchel-Type Min-Max Duality with Primal and Dual Integrality for M-Concave and M-Convex FunctionsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Convexity and Steinitz's Exchange Property I: The Extension Theorem — M-Concavity Is Concave Extendability with Integral Base Polytope MaximizersResearch Paper

Motivation

Setting

Formalization targets

Goal: the Extension Theorem (Theorem 4.6)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Komlos-Sulyok-Szemeredi bound: every finite set of reals has a Sidon subset of size c sqrt nResearch Paper

The exponent is the whole problem

The idea both proofs share

The two routes

Notes on the formalization

Conway's 99-graph problemOpen Problem

Motivation

Setting

Formalization targets

Goal

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

The Komlos ConjectureOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal — the Komlós conjecture

Milestones — the known ladder

Significance

Difficulty

Formalization scope

Selected references

Convexity and Steinitz's Exchange Property II: The Local Supermodularity Theorem for the Concave ConjugateResearch Paper

Motivation

Setting

Formalization targets

Goal: the Local Supermodularity Theorem (Theorem 5.3, corrected)

Milestones

Significance

Difficulty