Combinatorics

Motivation

In shop scheduling, jobs consist of chains of operations, each to be processed on a prescribed machine, and the goal is to minimize the makespan, the time at which the last operation finishes. Almost every approximation algorithm for job shops, acyclic job shops and flow shops is analysed against one quantity: the trivial lower bound $\mathrm{lb}=\max(C,D)$, where the congestion $C$ is the largest total processing time requested on one machine and the dilation $D$ is the largest total processing time of one job. Any schedule has makespan at least $\mathrm{lb}$.

How weak can this bound be? Leighton, Maggs and Rao (1994) showed that for acyclic job shops with unit-length operations the optimum is $O(\mathrm{lb})$. For operations of arbitrary length, Feige and Scheideler (2002) proved an upper bound of $O(\mathrm{lb}\cdot\log\mathrm{lb}\cdot\log\log\mathrm{lb})$ for acyclic job shops, and gave acyclic job shop instances whose optimum is $\Omega(\mathrm{lb}\cdot\log\mathrm{lb}/\log\log\mathrm{lb})$. Flow shops, in which every job visits every machine in one common order, are much more structured, and no flow shop instance with optimum $\omega(\mathrm{lb})$ was known. Feige and Scheideler asked whether flow shops admit a significantly better upper bound. Mastrolilli and Svensson (J. ACM 2011, Theorem 1.1) answered this negatively by constructing flow shops whose optimal makespan is a factor $\Omega(\log\mathrm{lb}/\log\log\mathrm{lb})$ above $\mathrm{lb}$.

Timeline:

• 1994 — Leighton, Maggs, Rao: unit-time acyclic job shops have optimum $O(\mathrm{lb})$ (packet routing).
• 2002 — Feige, Scheideler: upper bound $O(\mathrm{lb}\log\mathrm{lb}\log\log\mathrm{lb})$ for acyclic job shops, a nearly matching lower-bound family for acyclic job shops, and the open question for flow shops.
• 2011 — Mastrolilli, Svensson: flow shops with optimum $\Omega(\mathrm{lb}\log\mathrm{lb}/\log\log\mathrm{lb})$.

Setting

A job shop instance has machines and jobs; job $j$ is a sequence of operations $O_{1j},\dots,O_{\mu_j j}$, operation $O_{ij}$ needs $p_{ij}\ge0$ time units without interruption on machine $m_{ij}$. A feasible schedule assigns a start time $s\ge0$ to every operation so that each operation starts after the previous operation of its job has completed, and no two operations on one machine overlap. A zero-length operation therefore still occupies an instant on its machine: it cannot be performed strictly inside another operation there. The makespan $C_{\max}(s)$ is the largest completion time.

The instance $F(r,d)$, for natural numbers $r,d$:

• Machines. $r^{2d}$ groups $M_1,\dots,M_{r^{2d}}$; group $M_g$ has machines $m_{g,1},\dots,m_{g,d}$, one per frequency. The machines are ordered $m_{1,d},\dots,m_{1,1},m_{2,d},\dots,m_{2,1},\dots$: by group, and inside a group by decreasing frequency.
• Jobs. For each frequency $f=1,\dots,d$ there are $r^{2(d-f)}$ job groups $J^f_g$, each of $r^{2f}$ identical jobs. Such a job runs for $r^{2(d-f)}$ time units on each of the machines $m_{a+1,f},\dots,m_{a+r^{2f},f}$, $a=(g-1)r^{2f}$, and for $0$ time units on every other machine. Every job visits every machine in the common order, so $F(r,d)$ is a flow shop.

Operations of positive length are long-operations, the others short-operations. For a schedule, the $i$-th long-operation of a job $j$ of frequency $f$ is good if the delay $d_j(i)$ from its end to the start of the next long-operation of $j$ is at most $\frac{r^2}{4}r^{2(d-f)}$; the last long-operation of a job is never good. $T_{g,f}$ is the set of first halves $[s,s+p/2)$ of the good long-operations on machine $m_{g,f}$, and $L(T_{g,f})$ the total time they cover.

Formalization targets

Goal: Theorem 1.1, explicit form

For all natural numbers $r\ge8$ and $d$: every job of $F(r,d)$ has length $r^{2d}$, every machine has load $r^{2d}$ (so $\mathrm{lb}=r^{2d}$), and every feasible schedule $s$ satisfies

$$C_{\max}(s)\ \ge\ r^{2d}\cdot\min\Bigl(r,\ \frac d4\Bigr).$$

With $r=d$ this gives the paper's statement, an optimal makespan of $\Omega(\mathrm{lb}\cdot\log\mathrm{lb}/\log\log\mathrm{lb})$.

Milestones

• §2.2.1, p. 20:10: every job length and machine load equals $r^{2d}$.
• Lemma 2.2: if $C_{\max}(s)<r\cdot\mathrm{lb}$, every job has at least a $(1-4/r)$ fraction of good long-operations.
• Lemma 2.3: for $1\le k<\ell\le d$, the intervals of $T_{g,k}$ and $T_{g,\ell}$ are pairwise disjoint.
• Lemma 2.4: if $C_{\max}(s)<r\cdot\mathrm{lb}$, some group $g$ has $\sum_{f=1}^d L(T_{g,f})\ge\frac{\mathrm{lb}}4\cdot d$.

Significance

The theorem shows that the lower bound $\mathrm{lb}$, against which all known flow shop algorithms are analysed, can be off by a factor growing with $\mathrm{lb}$. Any flow shop algorithm with guarantee $o(\log\mathrm{lb}/\log\log\mathrm{lb})$ relative to the optimum must therefore use a stronger lower bound than $\max(C,D)$. The same frequency construction is the gap gadget behind the paper's inapproximability results for generalized flow shops and job shops (Theorems 1.2 and 1.3).

The result has been proved since 2011; as far as is known it has no machine-checked proof. The mission produces a formal model of the instance $F(r,d)$, a formal proof of the explicit bound for every $r\ge8$, $d$, and reusable statements about delays and first-half intervals in the published job shop model JobShopLTAS.Core.Instance.

Difficulty

The bound must hold for every feasible schedule, with no structural restriction such as a permutation or non-delay schedule. The obvious approach, comparing each machine's load with the makespan, only gives $C_{\max}\ge\mathrm{lb}$, since every machine carries exactly $\mathrm{lb}$. The gain comes from interaction between machines of different frequencies in one group: a high-frequency job running in parallel with a low-frequency long-operation is held back by its zero-length operation on the low-frequency machine. Turning this into a quantitative bound requires controlling, for every job at once, how long it waits between consecutive long-operations, and that waiting is only bounded when the makespan is already small. Encoding the index arithmetic of $F(r,d)$ (groups, frequencies, copies, positions of the long-operations) and the zero-length operations faithfully is a substantial part of the work.

Formalization scope

• Model. The published definition JobShopLTAS.Core.Instance: machines Fin m, jobs Fin n, real processing times and start times, IsFeasibleSchedule Finset.univ s (nonnegative starts, chain precedence, disjunctive machine constraint s o + p o ≤ s o' ∨ s o' + p o' ≤ s o) and makespan Finset.univ s. Under that constraint a zero-length operation cannot sit strictly inside another operation on its machine, which the paper's argument needs.
• Encoding. $F(r,d)$ has $r^{2d}d$ machines and $r^{2d}d$ jobs. Machine position $p$ is $m_{g,i}$ with $p=(g-1)d+(d-i)$, so position order is the paper's machine order. Job $q$ is $j^f_{g,a}$ with $q=(f-1)r^{2d}+(g-1)r^{2f}+(a-1)$. Every job has one operation per machine, the $i$-th on position $i$; frequencies, groups and copies are 1-based.
• Good operations. The next long-operation of a job is the next operation of positive length in its chain; a last long-operation is never good. $L(T)$ is the Lebesgue measure of the union of the intervals of $T$.
• Explicit constants replacing asymptotics. The paper's $\Omega(\mathrm{lb}\cdot\log\mathrm{lb}/\log\log\mathrm{lb})$ is replaced by the bound $r^{2d}\min(r,d/4)$ that §2.2.2 proves; the specialization $r=d$ and the asymptotic estimate $d=\Theta(\log\mathrm{lb}/\log\log\mathrm{lb})$ are not formalized. "Sufficiently large $r$" becomes $r\ge8$ (Lemma 2.4 and the goal: $1-4/r\ge1/2$) and $r\ge3$ (Lemma 2.3: $r^2/2-1>r^2/4$); Lemma 2.2 holds for every $r\ge1$. The standing assumption $C_{\max}<r\cdot\mathrm{lb}$ of §2.2.2 is an explicit hypothesis of Lemmas 2.2 and 2.4. "Optimal makespan" is stated as a bound on every feasible schedule.
• Ruled out. The goal quantifies over all feasible schedules of $F(r,d)$ as constructed; assuming the good-fraction or disjointness properties, restricting to permutation schedules, or a model in which zero-length operations occupy no machine time would trivialize or falsify it.
• Not in scope. The job shop warm-up of §2.1 (Lemma 2.1) and the reductions of §3–§4.

Welcome contributions: proofs of the counting facts about the encoding, of the milestones, and general lemmas about feasible schedules in JobShopLTAS.Core.Instance (completion time of a job bounds its delays; disjoint intervals in $[0,C_{\max}]$ have total length at most $C_{\max}$).

Selected references

• M. Mastrolilli, O. Svensson, Hardness of Approximating Flow and Job Shop Scheduling Problems, J. ACM 58(5), Article 20, 2011. https://doi.org/10.1145/2027216.2027218
• U. Feige, C. Scheideler, Improved Bounds for Acyclic Job Shop Scheduling, Combinatorica 22(3), 361–399, 2002. https://doi.org/10.1007/s004930200018
• F. T. Leighton, B. M. Maggs, S. B. Rao, Packet Routing and Job-Shop Scheduling in O(Congestion + Dilation) Steps, Combinatorica 14(2), 167–186, 1994. https://doi.org/10.1007/BF01215349
• P. Schuurman, G. J. Woeginger, Polynomial Time Approximation Algorithms for Machine Scheduling: Ten Open Problems, J. Scheduling 2(5), 203–213, 1999. https://doi.org/10.1002/(SICI)1099-1425(199909/10)2:5<203::AID-JOS26>3.0.CO;2-5

Motivation

A sparse graph that approximates a dense one, in the sense that both have nearly the same Laplacian quadratic form, can stand in for it in every algorithm that only reads cuts or solves Laplacian linear systems. Spielman and Teng introduced such spectral sparsifiers and built them in nearly linear time; the construction is the sparsification step of their nearly-linear-time Laplacian solver (arXiv:0808.4134, SIAM J. Comput. 40(4), 2011).

Sampling edges at random works well only inside a graph of high conductance, where no vertex set is separated from the rest by few edges. A general graph is therefore first cut into pieces of high conductance, with few edges running between the pieces. Section 7 of the paper proves that such a decomposition always exists. A similar result was obtained independently by Trevisan (2005). The decomposition theorem, together with the sampling theorem of §6, already shows that every graph has a spectral sparsifier with $O(n\log^7 n)$ edges; the algorithmic decomposition of §8, which the fast algorithm uses, is an approximate version of it, and its analysis rests on the same certificate lemma.

Setting

Let $G=(V,E)$ be a finite simple undirected graph with $m=|E|$ edges, and write $d_i$ for the degree of vertex $i$. For disjoint $S,T\subseteq V$, $E(S,T)$ is the set of edges with one end in $S$ and one in $T$. The volume of $S\subseteq V$ is $\operatorname{Vol}(S)=\sum_{i\in S}d_i$; in particular $\operatorname{Vol}(V)=2m$.

For a vertex set $B\subseteq V$ and $S\subseteq B$, the conductance of $S$ inside $B$ is

$$\Phi^G_B(S)=\frac{|E(S,B-S)|}{\min\big(\operatorname{Vol}(S),\operatorname{Vol}(B-S)\big)},\qquad \Phi^G_B(\emptyset)=1,$$

and the conductance of $B$ is $\Phi^G_B=\min_{S\subset B}\Phi^G_B(S)$ over proper subsets, with $\Phi^G_B=1$ when $|B|=1$. Volumes are always measured with the degrees of $G$, never with the degrees inside the induced subgraph $G(B)$; consequently $\Phi^G_B$ is at most the usual conductance of $G(B)$, and lower bounds on $\Phi^G_B$ transfer to it.

A decomposition of $G$ is a partition $(A_1,\dots,A_k)$ of $V$. It is a $\varphi$-decomposition if $\Phi^G_{A_i}\ge\varphi$ for all $i$, and its boundary is the set of edges between different parts,

$$\partial(A_1,\dots,A_k)=E\cap\bigcup_{i\neq j}(A_i\times A_j).$$

In Lean: vol G S, cutEdges G S T $=|E(S,T)|$, condRel G B S $=\Phi^G_B(S)$, cond G B $=\Phi^G_B$, and decompBoundary G P $=\partial(A_1,\dots,A_k)$ for a Finpartition P of the vertex set, all in the namespace SpectralSparsify.Decomp.

Formalization targets

Goal: Theorem 7.1 (p. 17)

Every graph $G$ without isolated vertices has a decomposition $(A_1,\dots,A_k)$ with

$$\Phi^G_{A_i}\ \ge\ \big(6\log_{4/3}2m\big)^{-1}\quad\text{for all } i,\qquad |\partial(A_1,\dots,A_k)|\ \le\ \frac{|E|}{2}.$$

The constants are the paper's. Both conditions must hold for one and the same partition.

Milestones

1. (12), first inequality (p. 18): for $S\subseteq B$, $R\subseteq B-S$, $T=R\cup S$, $|E(T,B-T)|\le|E(S,B-S)|+|E(R,B-S-R)|$.
2. The volume bound proving (13) (p. 19): if $\operatorname{Vol}(R)\le\frac12\operatorname{Vol}(B-S)$ and $\operatorname{Vol}(S)=\alpha\operatorname{Vol}(B)$, then $\operatorname{Vol}(R\cup S)\le\frac{1+\alpha}{2}\operatorname{Vol}(B)$.
3. Lemma 7.2, Sparsest Cuts as Certificates (p. 18): let $\varphi\le1$, and let $S\subset B$ maximize $\operatorname{Vol}(S)$ subject to (C.1) $\operatorname{Vol}(S)\le\operatorname{Vol}(B)/2$ and (C.2) $\Phi^G_B(S)\le\varphi$. If $\operatorname{Vol}(S)=\alpha\operatorname{Vol}(B)$ with $\alpha\le1/3$, then

$$\Phi^G_{B-S}\ \ge\ \varphi\,\frac{1-3\alpha}{1-\alpha}.$$

4. The $\varphi/3$ step (proof of Theorem 7.1, p. 19): under the hypotheses of Lemma 7.2 with $\operatorname{Vol}(S)\le\operatorname{Vol}(B)/4$, $\Phi^G_{B-S}\ge\varphi/3$.
5. The per-level cut bound (proof of Theorem 7.1, p. 19): for pairwise disjoint $B_1,\dots,B_r$ and $S_j\subset B_j$ satisfying (C.1) and (C.2) in $B_j$ with $\varphi\ge0$, $\sum_j|E(S_j,B_j-S_j)|\le\varphi|E|$.

Significance

The theorem says that every graph is, after removing at most half of its edges, a disjoint union of pieces of conductance $\Omega(1/\log m)$. By Cheeger's inequality each piece then has normalized spectral gap $\Omega(1/\log^2 m)$, which is the hypothesis under which the random sampling of §6 produces a spectral approximation; applying the theorem recursively to the removed edges gives the existence of spectral sparsifiers with $O(n\log^7 n)$ edges (§7.2). Decompositions of this kind, now called expander decompositions, have become a standard tool in graph algorithms.

The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. What the mission produces is a formal proof of the existence statement with the paper's explicit constant, a formal Lemma 7.2 (the certificate lemma that also drives the approximate version, Theorem 8.1), and reusable Lean definitions of volume, relative conductance $\Phi^G_B$ and decomposition boundary for finite simple graphs.

Difficulty

The obvious argument, cutting along any sparse set until no sparse set is left, controls the conductance of the final parts but not the number of edges cut: a long sequence of small sparse cuts can remove far more than half of the edges. The difficulty is to show that one well-chosen cut leaves a remainder whose conductance is certified without further search, which is the content of Lemma 7.2. Its hypothesis is a maximality condition over all subsets of $B$, and its conclusion concerns all subsets of $B-S$, a different set measured with the same ambient degrees, so the two cannot be compared directly. The existence statement then needs a well-founded description of the recursion, a bound on its depth, and an accounting of the cut edges level by level, all against the explicit constant $(6\log_{4/3}2m)^{-1}$.

Formalization scope

Graphs are SimpleGraph V on a finite vertex type with decidable adjacency; vertex sets are Finset V; volumes, conductances and the bound on $|\partial|$ are real numbers; decompositions are Finpartition (Finset.univ : Finset V); $\log_{4/3}$ is Real.logb (4/3).

Hypotheses made explicit:

• No isolated vertices (∀ v, 0 < G.degree v) in Theorem 7.1, Lemma 7.2 and the milestones that divide by a volume. The paper leaves it implicit: $\Phi^G_B(S)$ is $0/0$ for sets of isolated vertices, and with Lean's $0/0=0$ Lemma 7.2 would be false (one edge plus two isolated vertices is a counterexample). Under the hypothesis $m=0$ forces $V=\emptyset$, and Theorem 7.1 is then trivially true.
• $B$ nonempty in Lemma 7.2 and the $\varphi/3$ step, so that $\alpha=\operatorname{Vol}(S)/\operatorname{Vol}(B)$ is determined.
• $\varphi\ge0$ in the per-level bound (the paper's $\varphi$ is positive).

Conventions: $\Phi^G_B$ is the minimum over proper subsets, the empty set contributing $1$; $\Phi^G_B=1$ for $|B|\le1$; $|E(S,T)|$ counts ordered adjacent pairs in $S\times T$, which is the edge count for disjoint sets. Neither conclusion of Theorem 7.1 may be dropped: the partition into singletons satisfies the conductance bound and the partition into one part satisfies the boundary bound, so a formalization keeping only one conclusion is trivial.

Not formalized: idealDecomp as an object (step 2 involves a choice, so it is a relation rather than a function; the goal is the existence statement), its termination and depth bound as separate items, the λ-spectral decomposition remark via Cheeger's inequality, the existence sketch for sparsifiers in §7.2, and the algorithmic analogue of §8. Contributions welcome: proofs of the milestones, a formal recursion for idealDecomp, and lemmas on volume and edge-boundary arithmetic that other graph-partitioning missions can reuse.

Selected references

• D. A. Spielman, S.-H. Teng, Spectral Sparsification of Graphs, arXiv:0808.4134v3, 2010; SIAM J. Comput. 40(4), 2011. https://arxiv.org/abs/0808.4134
• L. Trevisan, Approximation algorithms for unique games, FOCS 2005, pp. 197–205; journal version Theory of Computing 4 (2008) 111–128. https://doi.org/10.4086/toc.2008.v004a005
• D. A. Spielman, S.-H. Teng, Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems, STOC 2004, pp. 81–90. https://doi.org/10.1145/1007352.1007372

Motivation

The dial-a-ride problem (DARP) asks for minimum-cost vehicle routes that carry users from individual pick-up points to individual drop-off points, subject to vehicle capacities, time windows, route durations and a bound on each user's ride time. It models door-to-door transport for elderly and disabled people, shared taxis and on-demand microtransit. Cordeau (Oper. Res. 54(3), 2006) gave a mixed-integer formulation of the DARP and the first branch-and-cut algorithm for it, and reported that instances with up to 30 users can be solved to optimality in reasonable time. The algorithm's strength comes from families of valid inequalities: linear constraints satisfied by every feasible route plan that cut off fractional points of the linear relaxation. Several of these families were adapted from the precedence-constrained asymmetric TSP (Balas, Fischetti and Pulleyblank 1995; Grötschel and Padberg 1985) and from the pick-up and delivery problem (Ruland and Rodin 1997); others, notably the generalized order-matching inequalities, were new in this paper.

Setting

Let $n$ be the number of users. Nodes are $N = \{0, 1, \dots, 2n+1\}$ with pick-up nodes $P = \{1,\dots,n\}$, drop-off nodes $D = \{n+1,\dots,2n\}$, origin depot $0$ and destination depot $2n+1$; user $i$ travels from node $i$ to node $n+i$. An instance fixes, for each node $i$, a load $q_i$, a service duration $d_i \ge 0$ and a time window $[e_i, l_i]$; for each pair of nodes a travel time $t_{ij}$; for each vehicle $k$ in a finite set $K$ a capacity $Q_k$ and a maximal route duration $T_k$; and a maximal ride time $L$. The standing conditions are $q_0 = q_{2n+1} = 0$, $q_i = -q_{n+i}$ for $i \in P$, and $d_0 = d_{2n+1} = 0$.

A feasible solution gives each vehicle $k$ a route $0 \to v_1 \to \dots \to v_r \to 2n+1$ through distinct nodes of $P \cup D$, start-of-service times $B^k_i$ and loads $Q^k_i$ such that every node of $P \cup D$ is visited by exactly one vehicle, $i$ and $n+i$ are on the same route with $i$ first, $B^k_j \ge B^k_i + d_i + t_{ij}$ and $Q^k_j \ge Q^k_i + q_j$ along each travelled arc, the ride time $B^k_{n+i} - (B^k_i + d_i)$ lies in $[t_{i,n+i}, L]$, the route lasts at most $T_k$, and the time windows and capacity bounds hold at every visited node. These are the constraints (2)–(14) of the paper's model.

The arc variables are $x^k_{ij} = 1$ when vehicle $k$ travels from $i$ to $j$, and $x_{ij} = \sum_{k \in K} x^k_{ij}$. For a node set $S$ write $\bar S = N \setminus S$, $x(S) = \sum_{i,j\in S} x_{ij}$, $x(\delta^+(S)) = \sum_{i\in S, j\in \bar S} x_{ij}$, $x(\delta^-(S)) = \sum_{i \in \bar S, j \in S} x_{ij}$, $\pi(S) = \{i \in P \mid n+i \in S\}$ and $\sigma(S) = \{n+i \in D \mid i \in S\}$. An inequality in $x$ is valid for the DARP when the aggregated arc variables of every feasible solution satisfy it.

Formalization targets

Goal: Proposition 5 (p. 578)

Let $i_1, \dots, i_m$ be distinct users and let $H, T_1, \dots, T_m \subseteq P \cup D$ satisfy $\{i_h, n+i_h\} \subseteq T_h$ and $H \cap T_h = \{i_h\}$. Then every feasible solution satisfies

$$x(H) + \sum_{h=1}^m x(T_h) \le |H| + \sum_{h=1}^m |T_h| - 2m. \tag{39}$$

The handle $H$ and the teeth $T_h$ are not required to be disjoint from one another beyond $H \cap T_h = \{i_h\}$, and $m$ is arbitrary.

Milestones (the steps of the proof of Proposition 5)

1. $x(S) \le |S| - 1$ for every nonempty $S \subseteq P \cup D$.
2. If $x(T) = |T| - 1$ for a set $T \ni i, n+i$, then a path of arcs with $x_{ab} = 1$ covers $T$ and does not finish at $i$.
3. With $\alpha$ the number of teeth for which $x(T_h) = |T_h| - 1$: $x(\delta^+(H)) \ge \alpha$.
4. $x(\delta^+(H)) = x(\delta^-(H))$ and $2x(H) + x(\delta^+(H)) + x(\delta^-(H)) = 2|H|$ for $H \subseteq P \cup D$.
5. $x(H) \le |H| - \alpha$.

Companion statements

The mission also states the other propositions of §4: the lifted subtour elimination inequalities (33) and (34) (Propositions 1 and 2), the predecessor inequality (30), the two liftings (36) and (37) of the generalized order constraint (Propositions 3 and 4), the redundancy of the strengthening (40) of (39) under (30) for fractional points (Proposition 6), and the infeasible path inequality (41) under the triangle inequality for travel times (Proposition 7).

Significance

Valid inequalities are what make branch-and-cut work: each family is added to the linear relaxation by a separation heuristic, and the paper's computational section reports how the bound improves as families are added. Validity is the one property the algorithm cannot check at run time, since a cut that removes a feasible route plan silently returns a suboptimal answer. Remark 2 of the paper observes that (39) is stronger than the TSP comb inequality on the same sets, and Proposition 6 shows that its natural strengthening adds nothing once the predecessor inequalities (30) are present, which tells an implementer which families to separate.

All propositions are proved in the paper, partly in an appendix; none is formalized. A machine-checked development would give a precise route-based model of the DARP that later DARP and pick-up and delivery papers can reuse, and certified validity of the cut families that branch-and-cut codes for these problems separate.

Difficulty

The proofs are short on paper but argue about the shape of routes: "there exists a path connecting all nodes in $T_h$", "this path cannot finish at node $i_h$ because of the precedence constraint". Turning a tight subtour count $x(T) = |T| - 1$ into a single covering path requires knowing that the arcs of a feasible solution inside a subset of $P \cup D$ form vertex-disjoint paths, which in turn rests on each node of $P \cup D$ having exactly one predecessor and one successor and on routes containing no cycles. The arithmetic step from $\alpha$ tight teeth to the bound on the handle needs the degree identities for every subset of $P \cup D$, and counting the arcs leaving $H$ needs the distinctness of the users $i_h$. Reasoning directly with the linear constraints (2)–(14) does not suffice: those constraints alone do not exclude cycles of zero duration.

Formalization scope

Nodes are natural numbers, so $n+i$ and $2n+1$ appear literally; $N$, $P$, $D$ and $P \cup D$ are Finset.range (2n+2), Icc 1 n, Icc (n+1) (2n) and Icc 1 (2n). All data and arc variables are real-valued, and every right-hand side is computed in $\mathbb R$. Feasible solutions are route-based: each vehicle has a duplicate-free list of nodes of $P \cup D$, and the constraints of the model are imposed along that list. Read literally, the program (1)–(14) admits closed cycles when $d_i + t_{ij} = 0$ around a cycle, on which every proposition fails, and imposes (11)–(13) also at nodes a vehicle does not visit; the route encoding follows the paper's verbal definition of the DARP and its proofs, which reason about routes. Precedence ($i$ before $n+i$) is a field of the solution, since with zero travel and service times the nonnegativity of ride times does not order the visits. The routing cost plays no role and is omitted. No positivity is assumed for travel or service times.

Added hypotheses, each necessary: sets $S$ in the subtour bound and in (30) are nonempty ($S = \emptyset$ gives $0 \le -1$); the users of Proposition 5 are distinct; the generalized order constraint (Propositions 3 and 4) has $m \ge 2$ (for $m = 1$ it is false); the ordered sets of Propositions 1 and 2 have $h \ge 3$ nodes, the standing assumption of the paragraph that introduces them; Proposition 7 has $p \ge 1$ and a path through distinct nodes. Proposition 6 is the only statement about fractional points: it assumes nonnegativity, no loops, (2), (3) and (30), and drops the remaining constraints of the relaxation, which makes it stronger.

The inequalities are stated for the arc variables of every feasible solution, not for an arbitrary $0$–$1$ vector satisfying a few degree constraints; a statement of the latter kind is a different and false theorem. Useful contributions include the path structure of the arcs of a feasible solution inside a subset of $P \cup D$, the degree identities, and the milestone proofs, which are reusable for the other propositions.

Selected references

• J.-F. Cordeau, A Branch-and-Cut Algorithm for the Dial-a-Ride Problem, Operations Research 54(3):573–586, 2006. https://doi.org/10.1287/opre.1060.0283
• E. Balas, M. Fischetti, W. R. Pulleyblank, The precedence-constrained asymmetric traveling salesman polytope, Mathematical Programming 68:241–265, 1995 (as cited in Cordeau 2006).
• M. Grötschel, M. W. Padberg, Polyhedral theory, in Lawler et al. (eds.), The Traveling Salesman Problem, Wiley, New York, 1985, pp. 251–305 (as cited in Cordeau 2006).
• K. S. Ruland, E. Y. Rodin, The pickup and delivery problem: Faces and branch-and-cut algorithm, Computers & Mathematics with Applications 33:1–13, 1997 (as cited in Cordeau 2006).

Motivation

The Heilbronn triangle problem asks how large the smallest triangle in an $n$-point set can be. A positive improvement in the exponent would contradict bounds at every scale arbitrarily close to $n^{-2}$. The source is OpenAI's September 2026 manuscript.

Setting

Points lie in the closed unit square in the real plane. Triangle area is half the absolute determinant of the two displacement vectors, and the lower-bound condition quantifies over all triples of distinct points.

Formalization targets

$$\delta>0,\quad n_j\to\infty,\quad |P_j|=n_j\ge3,\quad\min_{p,q,r\in P_j\text{ distinct}}\operatorname{Area}(pqr)\ge n_j^{-2+\delta}.$$

The Heilbronn exponent δ is positive and that there exist a sequence of natural numbers n(j) tending to infinity and finite sets P(j) of points in the plane, such that for every j, n(j) ≥ 3, P(j) has exactly n(j) points, all lying in the closed unit square [0,1]×[0,1], and every triple of three distinct points of P(j) spans a triangle of area at least n(j)^(−2+δ). Triangle area is |(q₁−p₁)(r₂−p₂)−(q₂−p₂)(r₁−p₁)|/2. Here δ = 1/(100000·K) with K = T²+1, where T = C(M,3), M = C(4·41−1, 41) = C(163,41), so δ is an explicit but extremely small positive rational constant. Thus the statement asserts an infinite family of point sets whose smallest triangle area is at least a power n^(−2+δ).

The goal is OAI.Problem355.heilbronn_power_lower_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• almost n minus two refuted.

Significance

The formal goal gives an unbounded sequence of configurations with a fixed explicit power improvement. An attached companion target rules out an eventual almost-$n^{-2}$ upper bound at half that exponent. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Avoiding collinear triples is insufficient: every nonzero triangle must also satisfy one uniform quantitative area bound. The exponent must stay positive independently of the size of the configuration.

Formalization scope

The selected goal asserts a sequence tending to infinity, rather than the stronger all-sufficiently-large-sizes statement in the manuscript. The explicit exponent is heilbronnExponent, built from fixed binomial coefficients. Finite sets eliminate repeated points; real powers specify the area scale.

The shared definitions are supplied by HeilbronnTriangle. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A power improvement in the Heilbronn triangle lower bound, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Random triangle deletion constructs a partial triangle packing. Its terminal uncovered edges measure how efficiently this process covers pairs, and the source seeks the leading constant rather than only the growth exponent. The source is OpenAI's September 2026 manuscript.

Setting

Start from the complete graph on $n$ vertices. At each step choose a remaining triangle uniformly and remove its three edges. A triangle-free state stays fixed. The terminal leave $F_n$ is the edge count at the end.

Formalization targets

$$\mathbb E\left[\left(\frac{F_n}{n^{3/2}}-\frac1{2\sqrt2}\right)^2\right]\to0,\qquad \frac{F_n}{n^{3/2}}\xrightarrow{\mathbb P}\frac1{2\sqrt2},\qquad \frac{\mathbb E F_n}{n^{3/2}}\to\frac1{2\sqrt2}.$$

For the random triangle-removal process, three limits hold as n tends to infinity. The process starts from the complete graph on n vertices, with graphs represented as sets of 2-element subsets of Fin n. At each step, if the current graph G contains triangles (3-subsets all of whose pairs are edges of G), one triangle is chosen uniformly at random and its three edges are deleted; if there is no triangle, the graph stays unchanged. Running this for C(n,2) steps gives the terminal law on graphs, and expectation and probability are taken with respect to it. Writing normalizedLeave(G) = |E(G)| / n^(3/2) and sharpConstant c = 1/(2√2), the theorem asserts: first, the expected value of (normalizedLeave(G) − c)² tends to 0; second, for every ε > 0, the probability that |normalizedLeave(G) − c| > ε tends to 0; and third, the expected number of edges of the terminal graph divided by n^(3/2) tends to c.

The goal is OAI.SharpTerminalLeave.sharp_terminal_leave.

Significance

The three conclusions record mean-square concentration, concentration in probability, and the limiting normalized expectation. The exact leading constant is part of the target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Early evolution estimates need to remain informative near termination, where triangles become scarce. A high-probability estimate alone need not control the second moment required here.

Formalization scope

Graphs are finite sets of pairs from Fin n, with transitions given by probability mass functions. Running for the initial edge count guarantees that the absorbing terminal law is reached. Expectations are finite sums and all limits are along natural $n$ tending to infinity.

The shared definitions are supplied by TriangleRemoval. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The sharp terminal leave in random triangle removal, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

High probability under independent coordinate sampling need not give a family any closure under unions. Discrete convexity asks whether a bounded number of its members nevertheless cover most sets in the stronger sense of inexpensive containment certificates. The source is OpenAI's September 2026 manuscript.

Setting

On Bernoulli product space $2^{[N]}$, each coordinate is present independently with probability $p$. For a family $D$, the exceptional family $E_k(D)$ consists of sets contained in no union of $k$ members of $D$. A family is $p$-small when it has containment generators with total cost at most $1/2$.

Formalization targets

$$\mu_p(D)\ge1-2^{-75}\quad\Longrightarrow\quad E_{2^{75}}(D)\text{ is }p\text{-small}.$$

For every positive integer N, every density p with 0<p<1, and every family D of subsets of the ground set {0,...,N-1} (an arbitrary family, with no monotonicity assumption), if the product measure of D under independent Bernoulli(p) coordinates, namely the sum over s in D of p^|s|(1-p)^(N-|s|), is at least 1 - 1/2^75, then the family of exceptional sets is small. Here the exceptional family for k=2^75 consists of all subsets S of the ground set that are contained in no union of k members of D, where the k members are given as an arbitrary tuple of exactly k entries of D, repeats allowed and with no disjointness required. A family A is small at density p if there is a family G of generator sets that covers A, meaning every member of A contains some member of G, and whose cost, the sum over I in G of p^|I|, is at most 1/2.

The goal is OAI.TalagrandDiscreteConvexity.talagrand_discrete_convexity.

Significance

The conclusion supplies explicit containment witnesses at the original density. A small probability for the exceptional event alone would not provide such a cover. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The family is arbitrary, so monotonicity cannot be used as an extra hypothesis. The same universal number of unions must work for all dimensions and all densities strictly between zero and one.

Formalization scope

Lean uses finite families of finite subsets of Fin N, with $N\ge1$ and $0<p<1$. A tuple has exactly $2^{75}$ entries; repetitions and overlaps are allowed. The cover cost counts each generator once. The separate two-union density-loss corollary is outside this goal.

The shared definitions are supplied by TalagrandDiscreteConvexity. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Talagrand’s discrete-convexity conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

An increasing property of a random set can be certified by small subsets. Fractional certificates allow weight to be spread across many subsets, so comparing them with ordinary certificates measures the cost of removing this relaxation. The source is OpenAI's September 2026 manuscript.

Setting

A cover is a family of generators such that every member of the increasing family contains a generator. A generator of size $s$ costs $p^s$. An ordinary cover and a fractional cover both have budget $1/2$; a fractional cover assigns weights in $[0,1]$ and supplies total weight at least one inside each member. The expectation thresholds $q$ and $q_f$ are suprema of feasible parameters in $[0,1]$.

Formalization targets

$$q_f(\mathcal F)\le 25\cdot512^4\,q(\mathcal F).$$

For a finite nonempty ground type α and a family F of subsets of α that is nonempty, is not the entire power set, and is increasing (any superset of a member of F is again in F), the fractional threshold qf(F) is at most 25·512⁴ times the integral threshold q(F). Here q(F) is the supremum of those p in [0,1] for which F is small: some family G of sets covers F, meaning every H in F contains a member of G, with total cost Σ_{S∈G} p^{|S|} at most 1/2. The fractional threshold qf(F) is the analogous supremum of p in [0,1] for which there is a weight function g from subsets of α to [0,1] such that every H in F has Σ_{S⊆H} g(S) ≥ 1 and the fractional cost Σ_S g(S)·p^{|S|} is at most 1/2.

The goal is OAI.TalagrandThreshold.talagrand_expectation_threshold_equivalence.

Significance

The comparison gives a dimension-independent bound with the same budget on both sides. It isolates certificate rounding from the separate question of locating the random-set threshold. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Replacing fractional weights independently can lose control of covering every member simultaneously. The constant must be independent of both ground-set size and the sizes of weighted sets.

Formalization scope

The ground type is finite and nonempty, and the family is nonempty, proper, and increasing. Costs are finite real sums and thresholds are real suprema. The exact constant in the published goal is retained; the objective is this inequality, not an unspecified equivalent comparison.

The shared definitions are supplied by TalagrandExpectationThreshold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Integral and fractional expectation thresholds are equivalent, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

List coloring permits each vertex to have different allowable colors. The mission asks whether the size of the largest clique minor still controls the required list size up to a universal linear factor. The source manuscript presents the surrounding research claim.

Setting

A clique minor of order t is represented by disjoint connected vertex sets, with an edge between every pair. The Hadwiger number h(G) is the largest possible t. The list chromatic number is the least k for which every assignment of at least k colors per vertex admits a proper selection.

Formalization target

Prove one integer C≥1 works for every finite nonempty simple graph:

$$\chi_{list}(G)\le C\,h(G).$$

The constant is chosen before the graph, the vertex type and all color lists.

The selected formal target is OAI.LinearListHadwiger.main_theorem.

Significance and status

The assertion controls list coloring rather than only a common-color-set chromatic number. It is a linear-factor statement, without coefficient-one optimality. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A coloring from one chosen palette need not respect independently assigned lists. The proof must cover arbitrary color types and list assignments.

Formalization scope

The definitions use finite graph vertex types, arbitrary finite color sets, induced-subgraph connectivity and natural-number infima/suprema. Nonemptiness of the vertex type is explicit. Only the main inequality and its definition block are attached.

Selected references

• OpenAI, A linear list-coloring bound in terms of the Hadwiger number, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A tile may admit a translation tiling while forcing every such tiling to lack a full lattice of periods. The mission asks for this phenomenon in dimension three and its persistence under Euclidean thickening. The source manuscript presents the surrounding research claim.

Setting

A finite nonempty integer tile T⊆ℤᵈ tiles with complement A when addition T×A→ℤᵈ is bijective. Full periodicity means invariance under a finite-index subgroup. The thickening is the union of closed unit cubes based at T; Euclidean tiling means unique covering almost everywhere.

Formalization target

Construct T⊆ℤ³ that tiles but has no fully periodic complement, and whose thickening tiles ℝ³ but has no complement invariant under any full-rank lattice. Also prove

$$\min\{d:\text{an integer tile without a periodic complement exists in }\mathbb Z^d\}=3.$$

The selected formal target is OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality.

Significance and status

The goal includes both discrete and arbitrary-real-translation Euclidean assertions, plus minimality among all natural dimensions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Excluding periodic integer translation sets does not automatically exclude Euclidean tilings with noninteger shifts. The latter universal quantifier is a separate clause.

Formalization scope

Discrete tilings are exact bijections, whereas Euclidean tilings are almost-everywhere unique representations relative to Lebesgue measure. Euclidean full periodicity uses the integer span of a real basis. Closed-cube overlaps are handled by the almost-everywhere convention.

Selected references

• OpenAI, A translational tile with no fully periodic tiling in dimension three, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

At its critical weight, a self-avoiding path on the honeycomb lattice can make long excursions without paying an exponential cost. A basic quantitative question is how much of its total weight reaches the far side of a strip of height $N$. Physics heuristics (Nienhuis's Coulomb gas and the conjectured $\mathrm{SLE}_{8/3}$ scaling limit with boundary exponent $5/8$) predict that this crossing mass decays like $N^{-1/4}$. Rigorous results so far showed only that it tends to zero, with a polynomial upper bound with a tiny exponent.

The OpenAI preprint behind this mission, dated September 26, 2026 (source), claims the predicted power with bounded-factor constants: the crossing mass is comparable to $N^{-1/4}$, and the first horizontal-displacement moment of paths returning to the starting side is comparable to $N^{3/4}$ (Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1982 — Nienhuis's Coulomb-gas analysis of the dilute $O(n)$ model predicts the honeycomb critical point $\sqrt{2+\sqrt2}$ and the planar self-avoiding-walk exponents, including $\nu=3/4$ (PRL 1982).
• 2004 — Lawler, Schramm and Werner describe the conjectural $\mathrm{SLE}_{8/3}$ scaling limit; the boundary exponent $5/8$ predicts a crossing power $-1/4$ for strips.
• 2012 — Duminil-Copin and Smirnov prove that the connective constant of the honeycomb lattice is $\sqrt{2+\sqrt2}$ using a parafermionic observable and a boundary identity (Annals 2012); their strip argument bounds the crossing mass between orders $1/N$ and $1$.
• 2014 — Beaton, Bousquet-Mélou, de Gier, Duminil-Copin and Guttmann prove that the critical bridge mass tends to zero (CMP 2014).
• 2020 — Glazman and Manolescu give a shorter proof and a quantitative bound along a subsequence of heights (AIHP 2020).
• 2026 — Krachun and Panagiotis prove a polynomial upper bound on the bridge mass and quantitative sub-ballisticity (Ann. Probab. 2026).
• September 2026 — A group of OpenAI preprints claims the strip crossing power $-1/4$ with bounded-factor constants (source), the bridge mean-length exponent $4/3$ (source), and spatial exponent $3/4$ for several laws of critical walks (source).

Setting

Use the honeycomb lattice dual to the equilateral triangular tiling of side one, with one edge direction horizontal; its vertices are the triangles up i j and down i j, where $j\ge0$ indexes the horizontal band. Let $S_N$ be the strip of $N$ bands. A path starts in the triangle up 0 0 (just above bottom port $0$), visits distinct triangles, moves between adjacent ones, and stays in bands $0,\dots,N-1$. Its length $|\gamma|$ is the number of visited triangles and its critical weight is $\rho^{|\gamma|}$ with $\rho=(2+\sqrt2)^{-1/2}$. An arch ends at up k 0 with $k\neq0$ (bottom port $k$); a bridge ends at a down triangle of the top band. Put $c=\cos(3\pi/8)$ and

$$K_N(k)=\sum_{\text{arches to }k}\rho^{|\gamma|},\quad A_N=\sum_{k\ne0}K_N(k),\quad B_N=\sum_{\text{bridges}}\rho^{|\gamma|},\quad m_N=\sum_{k\ge1}k\,K_N(k).$$

Write $f_N\asymp g_N$ if $\ell g_N\le f_N\le u g_N$ for all $N\ge1$ with fixed constants $\ell,u>0$.

Formalization targets

Goal: Theorem 1.1 (Critical strip mass, p. 2)

For every $N\ge1$ all sums above are finite, and with constants independent of $N$,

$$cA_N+B_N=1,\qquad m_{N+1}-m_N\asymp B_N,\qquad m_N\asymp N^{3/4},\qquad B_N\asymp N^{-1/4},$$

and $B_N$ is nonincreasing in $N$.

Significance

The result itself. It establishes the predicted crossing power $-1/4$ with uniform multiplicative constants, not just a logarithmic exponent, improving the qualitative decay of Beaton et al. and the polynomial upper bound of Krachun and Panagiotis. It is an input for the bridge-length and spatial-exponent results of companion preprints. The exponent of $m_N$ concerns an unnormalized displacement moment summed over all lengths; the fixed-length displacement conjecture and the scaling limit are different questions.

Formalizing it. The proof combines an exact boundary identity of Duminil-Copin–Smirnov type, finite-strip transfer matrices with integrable local relations, a Pfaffian that makes the stationary vector polynomial, and a comparison of the resulting positive integral with Bures–Laguerre ensembles. A formal proof would include the honeycomb boundary identity, the core of the connective-constant proof, which is itself a natural formalization target. No machine-checked honeycomb walk result of this kind is known.

Difficulty

The boundary identity $cA_N+B_N=1$ (Lemma 4.2, p. 15) does not determine the power: it only gives $B_N$ between orders $1/N$ and $1$. The preprint's route computes the arch moment $m_N$ first, as one coefficient of a ratio $p_{N+1}/p_N$ of Pfaffians (Proposition 4.1, p. 13), converts it into a positive $N$-fold integral with Bures-type interaction (Section 5), and estimates that integral uniformly in $N$ by comparison with Laguerre laws (Section 6). The crossing power then follows from monotonicity and $m_{N+1}-m_N\asymp B_N$. A degree bound on the polynomial vacuum (Lemma 3.2, p. 10) is essential, because it turns interpolation into an identity argument.

Formalization scope

• Triangles are ℤ × ℕ × Bool (column, band, up/down); adjacency joins an up triangle to the down triangles sharing an edge. Paths are Lists with Nodup, IsChain adjacent, head up 0 0, a prescribed last triangle, and all bands < N.
• Weights are rho ^ p.length on paths satisfying IsPath, and 0 otherwise; all masses are tsums over lists. The goal includes summability of each family, so the tsums are genuine sums.
• moment N = ∑' k : ℕ, (k+1) * K N (k+1), i.e. $\sum_{k\ge1}kK_N(k)$.
• Comparable f g asks for constants $0<\ell,u$ with $\ell g(N)\le f(N)\le ug(N)$ for every $N\ge1$; powers are real rpow.
• Monotonicity is $B_{N+1}\le B_N$ for $N\ge1$.

Reusable contributions: the honeycomb boundary (parafermionic) identity in finite domains, and summability of critical walk weights in strips.

Selected references

• OpenAI, Critical strip-crossing mass on the honeycomb lattice, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-strip-crossing-mass-on-the-honeycomb-lattice-September-26-2026/main.pdf
• G. F. Lawler, O. Schramm, W. Werner, On the scaling limit of planar self-avoiding walk, Proc. Sympos. Pure Math. 72, Part 2 (2004), 339–364.
• Y. Ikhlef, J. Cardy, Discretely holomorphic parafermions and integrable loop models, J. Phys. A 42 (2009), 102001. https://doi.org/10.1088/1751-8113/42/10/102001
• A. Glazman, Connective constant for a weighted self-avoiding walk on $\mathbb Z^2$, Electron. Commun. Probab. 20 (2015), paper 86. https://doi.org/10.1214/ECP.v20-3844
• B. Nienhuis, Exact critical point and critical exponents of O(n) models in two dimensions, Phys. Rev. Lett. 49 (1982), 1062–1065. https://doi.org/10.1103/PhysRevLett.49.1062
• H. Duminil-Copin, S. Smirnov, The connective constant of the honeycomb lattice equals $\sqrt{2+\sqrt2}$, Ann. of Math. 175 (2012), 1653–1665. https://doi.org/10.4007/annals.2012.175.3.14
• N. R. Beaton, M. Bousquet-Mélou, J. de Gier, H. Duminil-Copin, A. J. Guttmann, The critical fugacity for surface adsorption of self-avoiding walks on the honeycomb lattice is $1+\sqrt2$, Comm. Math. Phys. 326 (2014). https://doi.org/10.1007/s00220-014-1896-1
• A. Glazman, I. Manolescu, Self-avoiding walk on $\mathbb Z^2$ with Yang–Baxter weights: universality of critical fugacity and 2-point function, Ann. Inst. H. Poincaré Probab. Statist. 56 (2020). https://doi.org/10.1214/19-AIHP1024
• D. Krachun, C. Panagiotis, Quantitative sub-ballisticity of self-avoiding walk on the hexagonal lattice, Ann. Probab. 54 (2026), 1109–1125. https://doi.org/10.1214/24-AOP1730

Motivation

Random 3-SAT, a conjunction of random three-literal clauses on $n$ variables, is the classic test case for the typical behavior of satisfiability. Experiments placed the hardest instances near the density where half the formulas are satisfiable, and statistical physics predicts a sharp satisfiability threshold near $4.267$. Once a limiting threshold $\alpha_3$ is known to exist, a natural question is whether it is a computable real: is there an algorithm that, given $r$, outputs a rational within $2^{-r}$ of $\alpha_3$? Existence alone does not imply this, since limits of computable sequences need not be computable (Specker 1949). This mission asks for such an algorithm.

Timeline

• 1949. Specker constructs a bounded monotone computable sequence of rationals with a noncomputable limit.
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp transition about a size-dependent location (doi:10.1090/S0894-0347-99-00305-7).
• 2003, 2006. Hajiaghayi and Sorkin, and Kaporis, Kirousis and Lalas, prove the lower bound $3.52$ (arXiv:math/0310193).
• 2002–2006. Mézard, Parisi and Zecchina develop the cavity/survey-propagation picture; Mertens, Mézard and Zecchina predict $\alpha_3\approx4.267$.
• 2009. Díaz, Kirousis, Mitsche and Pérez-Giménez prove the upper bound $4.4898$.
• 2013. Bayati, Gamarnik and Tetali prove limits for normalized optimization values via sparse interpolation (doi:10.1214/12-AOP816).
• 2022. Ding, Sly and Sun prove the satisfiability conjecture with the predicted value for all large $k$ (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves a polynomial scaling window and the existence of limiting thresholds for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026); priority for the satisfiability conjecture belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 27, 2026. Its contribution is computability of $\alpha_3$, beyond existence.

Setting

For $n\ge3$, a proper random 3-clause chooses three distinct variables uniformly from $x_1,\dots,x_n$ and gives each an independent fair sign. Let $\Phi(n,m)$ be the conjunction of $m\ge0$ independent such clauses (sampled with replacement from the $8\binom n3$ possibilities; the empty formula is satisfiable) and

$$p(n,m)=\mathbb P\{\Phi(n,m)\ \text{is satisfiable}\}.$$

A real $\alpha$ is computable if a single algorithm, on input $r$, halts with a rational $q_r$ satisfying $|q_r-\alpha|\le2^{-r}$.

Formalization targets

Goal: Theorem 1.1

There is $\alpha_3\in(0,\infty)$ such that for every fixed real $a\ge0$

$$\lim_{n\to\infty}p(n,\lfloor an\rfloor)=\begin{cases}1,&a<\alpha_3,\\0,&a>\alpha_3,\end{cases}$$

and one finite deterministic Turing machine, on input $1^r$, halts with a rational $q_r$ with $|q_r-\alpha_3|\le2^{-r}$, using no oracle, advice, or noncomputable constant. Lean: OAI.FixedClauseThreshold.Computability.main, open on the platform.

Significance

The theorem makes the random 3-SAT threshold an effectively approximable constant: in principle its digits can be certified, although no efficiency bound is obtained. The method produces two families of finite certificates, rational lower bounds from a deletion estimate and rational upper bounds from finite hierarchical approximations of a soft pressure, and a fair search over them halts without any computable rate of finite-size convergence. The paper also gives a self-contained existence proof of $\alpha_3$ (Theorem 4.4) for the same proper-clause model.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Finite-size satisfiability probabilities are computable, but their convergence rate is unknown, so truncating at a finite $n$ certifies nothing. Lower certificates need an explicit bound on how far the finite-size centers can lie above the limit. Upper certificates are harder: one must show that above $\alpha_3$ some finite, checkable object witnesses unsatisfiability in the limit. This requires a variational (Parisi-type) description of the limiting pressure of the soft constraint model, approximated by finitely many rational parameters with a proof that the approximation is complete at every rational density above the threshold.

Formalization scope

• ProperClause n k is Fin n → Option Bool with exactly $k$ defined entries; Formula n k m := Fin m → ProperClause n k; properSATProbability n 3 m is the exact counting ratio, equal to $p(n,m)$.
• MainStatement asserts $\exists\,\alpha>0$ with the two strict-side limits at $m=\lfloor an\rfloor$, a sequence q : ℕ → ℚ with Computable (fun r => encode (q r)), a Nat.Partrec.Code c with c.eval r = some (encode (q r)), and $|q_r-\alpha|\le2^{-r}$ for all $r$.
• The input is a natural number rather than a unary string, which is equivalent for computability; the $r=0$ case is a harmless extra requirement.
• Nothing is asserted at $a=\alpha_3$.

Infrastructure: Mathlib's Computable/Nat.Partrec.Code, finite counting for random formulas, Poisson clause processes, interpolation bounds, and Ruelle cascades for the upper certificates. Formalizations of Lemma 2.1 (finite-certificate search, purely computability-theoretic and reusable), Theorem 4.4 and Theorem 8.4 are welcome.

Selected references

• OpenAI, Computing the Random 3-SAT Threshold, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026/article.pdf
• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
• M. Hajiaghayi, G. B. Sorkin, The satisfiability threshold of random 3-SAT is at least 3.52, preprint, 2003. https://arxiv.org/abs/math/0310193
• D. Panchenko, The Parisi ultrametricity conjecture, Ann. of Math., 2013. https://doi.org/10.4007/annals.2013.177.1.8
• E. Specker, Nicht konstruktiv beweisbare Sätze der Analysis, J. Symbolic Logic, 1949.

Motivation

Random planar maps are graphs embedded in the sphere, chosen at random; they are the discrete models of two-dimensional quantum gravity. Decorating a map with a Fortuin–Kasteleyn (FK) random-cluster configuration with parameter $q$ couples the geometry of the map to a statistical-mechanics model (percolation, Ising, Potts), and the coupling changes the large-scale shape of the map. For $0<q<4$ the maps are expected to converge to Liouville quantum gravity surfaces; for $q>4$ the cluster weight is so strong that the map is predicted to become tree-like at large scales. This mission concerns that tree-like regime.

Timeline

• 1963. Tutte decomposes planar maps into nonseparable blocks (doi:10.4153/CJM-1963-029-x).
• 1967. Mullin enumerates tree-rooted maps (doi:10.4153/CJM-1967-010-x).
• 1972. Fortuin and Kasteleyn introduce the random-cluster model (doi:10.1016/0031-8914(72)90045-6).
• 1993. Aldous introduces the Brownian continuum random tree (CRT) as the limit of finite-variance conditioned Galton–Watson trees (doi:10.1214/aop/1176989404).
• 2007–2008. Bernardi gives bijective encodings of tree-rooted maps and connects them to the Tutte polynomial (doi:10.37236/928).
• 2016. Sheffield's inventory-accumulation (hamburger–cheeseburger) bijection encodes FK-decorated maps and identifies the transition at $q=4$; his appendix predicts a CRT limit for $q>4$ (doi:10.1214/15-AOP1061). Panagiotou, Stufler and Weller prove CRT limits for subcritical graph classes (doi:10.1214/15-AOP1048).
• 2026. Feng proves an infinite-volume counterpart: an infinite FK map with $q>4$ converges to an infinite CRT in the local Gromov–Hausdorff–Prokhorov topology (doi:10.1007/s00440-025-01424-2); Stufler proves degree-measure CRT limits for maps whose block weights depend only on block size (arXiv:2608.21063).

The source of this mission, an OpenAI preprint dated September 24, 2026, proves the finite-volume CRT prediction for every $q>4$.

Setting

A rooted planar map is a connected graph embedded in the oriented sphere, up to orientation-preserving homeomorphism, with a distinguished dart (oriented edge); loops and multiple edges are allowed. For an edge subset $A\subseteq E(M)$, $k_M(A)$ is the number of connected components of $(V(M),A)$, isolated vertices included. For $q>4$ and $n\ge1$, sample $(M_n,A_n)$ with $|E(M_n)|=n$ according to

$$\mathbb P\bigl((M_n,A_n)=(M,A)\bigr)=\frac{1}{Z_{n,q}}\,q^{\,k_M(A)+(|A|-|V(M)|)/2}.$$

Let $d_n$ be graph distance on $V(M_n)$ using all edges and $\mu_n(\{v\})=\deg(v)/(2n)$.

For a standard normalized Brownian excursion $e$ on $[0,1]$, $d_e(s,t)=e(s)+e(t)-2\min_{[s\wedge t,\,s\vee t]}e$; the quotient by $d_e=0$ with the pushforward $\mu_e$ of Lebesgue measure is the Brownian CRT $(\mathcal T_e,d_e,\mu_e)$.

The Gromov–Hausdorff–Prokhorov (GHP) distance between compact metric probability spaces is the infimum, over isometric embeddings into a common space, of the maximum of the Hausdorff distance of the images and the Lévy–Prokhorov distance of the pushed-forward measures.

Formalization targets

Goal: Theorem 1.1

$$\forall q>4\ \exists c(q)\in(0,\infty):\qquad \bigl(V(M_n),\ c(q)\,n^{-1/2}d_n,\ \mu_n\bigr)\ \Longrightarrow\ (\mathcal T_e,d_e,\mu_e)$$

in distribution for the GHP topology, as $n\to\infty$ through all positive integers. The Lean statement OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt is open on the platform.

Significance

The theorem establishes the tree side of the geometric phase transition of FK planar maps at $q=4$ in the natural finite-volume setting: the law is conditioned on the total size, the metric uses every edge, and the measure is the degree measure. Feng's infinite-volume result does not imply it, and a limit of an unconditioned encoding walk gives neither conditioning nor metric control. Together with companion results for $0<q\le4$, it completes the picture surface versus tree.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would also build reusable infrastructure: combinatorial maps as rotation systems, the GHP topology, and the Brownian CRT, none of which is in Mathlib.

Difficulty

The FK weight of a nonseparable block depends on its shape, not only on its size, so the block-weighted map results with uniform blocks do not apply, and exponential moments of block sizes are not available. The proof must show that the block tree is a critical Galton–Watson tree with finite offspring variance, and that graph distance along every ancestral path is asymptotically a constant times the depth, uniformly over all paths, using only a second moment.

Formalization scope

• A map with $n+1$ edges is a pair of permutations of Fin (2*(n+1)) (edge involution without fixed points, vertex rotation), connected, with $|V|+|F|=n+3$ (genus zero), modulo isomorphisms fixing dart 0. The Lean index $n$ corresponds to $n+1$ edges, and the scale is $c/\sqrt{n+1}$.
• The FK law sums over all Finsets of edge orbits; clusterCount counts components including isolated vertices; loops are omitted from adjacency only.
• MetricMeasureData packages a carrier, a distance and a measure; Valid means a compact metric probability space with Borel σ-algebra. ghpEDist is the infimum over pseudometrics on the disjoint union extending both distances.
• Convergence in distribution is expressed by expectations of bounded tests F continuous for ghpEDist at valid objects.
• The normalized excursion is realized as $\lvert B(t)-tB(1)\rvert$ for a three-dimensional Brownian motion $B$, and the statement holds for every such realization. The limit expectation is a Bochner integral, so measurability of the integrand is part of what must be proved.

A complete development needs Sheffield's inventory bijection or an equivalent finite word identity, Tutte's block decomposition, conditioned Galton–Watson tree limits with finite variance (Aldous; Broutin–Marckert), and GHP comparison lemmas. Contributions formalizing Proposition 2.2 (finite word identity), Proposition 4.3 (exact finite representation), Theorem 5.5 (uniform marked path sums) and Lemma 6.3 (metric and mass comparison) are welcome.

Selected references

• OpenAI, Brownian continuum random tree limits of finite Fortuin–Kasteleyn maps above four, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Brownian-continuum-random-tree-limits-of-finite-Fortuin-Kasteleyn-maps-above-four-September-24-2026/main.pdf
• S. Sheffield, Quantum gravity and inventory accumulation, Ann. Probab., 2016. https://doi.org/10.1214/15-AOP1061
• Y. Feng, Triviality of critical Fortuin–Kasteleyn decorated planar maps for $q>4$, Probab. Theory Related Fields, 2026. https://doi.org/10.1007/s00440-025-01424-2
• D. Aldous, The continuum random tree III, Ann. Probab., 1993. https://doi.org/10.1214/aop/1176989404
• C. M. Fortuin, P. W. Kasteleyn, On the random-cluster model I, Physica, 1972. https://doi.org/10.1016/0031-8914(72)90045-6
• W. T. Tutte, A census of planar maps, Canad. J. Math., 1963. https://doi.org/10.4153/CJM-1963-029-x
• N. Broutin, J.-F. Marckert, Asymptotics of trees with a prescribed degree sequence and applications, Random Structures Algorithms, 2014. https://doi.org/10.1002/rsa.20463
• K. Panagiotou, B. Stufler, K. Weller, Scaling limits of random graphs from subcritical classes, Ann. Probab., 2016. https://doi.org/10.1214/15-AOP1048
• B. Stufler, Non-bijective scaling limits and phase transitions of planar maps, preprint, 2026. https://arxiv.org/abs/2608.21063

Motivation: tensor squares that contain everything

The irreducible complex representations of the symmetric group $S_n$ are indexed by partitions $\lambda\vdash n$ and written $S^\lambda$ (Specht modules). Decomposing a tensor product $S^\lambda\otimes S^\mu$ (with the diagonal action) into irreducibles is governed by the Kronecker coefficients

$$g(\lambda,\mu,\nu)=\dim\operatorname{Hom}_{S_n}\!\big(S^\nu,\,S^\lambda\otimes S^\mu\big),$$

which have no known positive combinatorial formula and are a central open topic in algebraic combinatorics and geometric complexity theory. A basic test of how far tensor products spread is the tensor square conjecture: in every degree (with a few exceptions) some single irreducible representation has a tensor square containing every irreducible representation.

Timeline

• 2012 — Saxl proposes (UCLA Combinatorics Seminar, 20 March 2012) that the staircase $\rho_m=(m,m-1,\dots,1)$ at triangular degree $n=m(m+1)/2$ has this property; recorded by Pak, Panova and Vallejo.
• 2013 — Heide, Saxl, Tiep and Zalesski conjecture an analogous covering property for alternating simple groups (HSTZ 2013, Rem. 1.3(3)).
• 2013/2016 — Pak, Panova and Vallejo state the tensor square conjecture for $n\ge3$, $n\ne4,9$, and the Saxl conjecture, and give a character-nonvanishing criterion (PPV 2016, Conj. 1.1–1.2, Lemma 1.3).
• 2015 — Ikenmeyer proves the staircase assertion for all $\nu$ comparable with the staircase in dominance order (Ikenmeyer 2015, Thm 2.1).
• 2017 — Luo and Sellke: staircase squares contain almost all partitions, and fourth powers cover everything in large degree (Luo–Sellke 2017).
• 2018 — Bessenrodt: all double-hook constituents (Bessenrodt 2018, Thm 4.10).
• 2021 — Li: the triple-hook case, and a conjectured family for nontriangular degrees (Li 2021).
• 2023 — Harman and Ryba: staircase tensor cubes contain everything (Harman–Ryba 2023, Thm 1.1).
• 2026 — An OpenAI preprint, Universal Tensor Squares for Symmetric Groups (OpenAI Math Release, September 24, 2026), claims the tensor square conjecture for every $n\notin\{2,4,9\}$, building on a companion preprint that proves Saxl's conjecture in a cyclic form. Neither preprint is peer reviewed and the main theorem is not formally verified; its proof uses exact computer calculations for degrees up to $64$.

Setting

For a Young diagram $\lambda$ with $n$ cells, fix a bijection $t$ between $\{0,\dots,n-1\}$ and the cells (a tableau). The Lean development realizes $S^\lambda$ inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$ ($d$ = number of rows), with $S_n$ acting by permuting letters: the polytabloid $e_t$ is the signed sum, over the column group of $t$, of the permuted indicator of the row word of $t$, and Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The Kronecker coefficient kronecker a b t is finrank of the space of $S_n$-intertwining maps from spechtRep t to the tensor product spechtRep a ⊗ spechtRep b. canonicalTableau λ is a fixed tableau of shape $\lambda$.

Formalization targets

Goal: a universal tensor square in every degree $n\notin\{2,4,9\}$

For every positive integer $n$ with $n\ne2,4,9$ there is a partition $\lambda\vdash n$ such that

$$g(\lambda,\lambda,\nu)>0\qquad\text{for every }\nu\vdash n ,$$

so the tensor square $S^\lambda\otimes S^\lambda$ contains every irreducible representation of $S_n$. The Lean statement asserts, for one Young diagram $\lambda$ with $n$ cells: positivity of kronecker for every target diagram $\nu$ with $n$ cells; irreducibility of spechtRep for $\lambda$; and that every finite-dimensional irreducible complex representation of $S_n$ admits an injective intertwining map into $S^\lambda\otimes S^\lambda$. This is Theorem 1.1 of the source together with its "thus" sentence. The goal is published on the platform with status Open.

Significance

The result itself. The theorem settles the tensor square conjecture of Pak, Panova and Vallejo, including all nontriangular degrees. Since the sign representation occurs, the chosen $\lambda$ must be self-conjugate. Via Letellier's results it also gives tensor squares of unipotent characters of $\mathrm{GL}_n(\mathbb F_q)$ that contain every unipotent character (Corollary 1.2 of the source). The companion cyclic Saxl theorem is used as input at staircase degrees.

Formalizing it. The proof combines representation-theoretic constructions with exact finite computations (Murnaghan–Nakayama recursion for all eligible $n\le64$, and capacity calculations), which the source certifies by included programs. A formal proof would replace these with checked computation and would require building Specht modules, Kronecker coefficients and branching rules in Lean, infrastructure Mathlib currently lacks.

Difficulty

Knowing that a smaller staircase square contains every constituent does not transfer to an enlarged diagram: constituents must survive a map from the actual enlarged tensor square, and the attached cells introduce alternating terms that can cancel. Almost-all or higher-power results (Luo–Sellke, Harman–Ryba) do not give a universal square. Small degrees cannot be handled by asymptotic estimates and require exact Kronecker computations, and $n=2,4,9$ are genuine exceptions.

Formalization scope

• Partitions are Mathlib YoungDiagrams with card = n; the representation space is (Fin n → Fin d) → ℂ, and Specht t is the cyclic span of one polytabloid. kronecker is Module.finrank ℂ of Representation.IntertwiningMap, so it is the genuine multiplicity of $S^\nu$ in the tensor square.
• The third conjunct quantifies over all finite-dimensional complex irreducible representations in a fixed universe; proving it requires that every irreducible of $S_n$ is isomorphic to some Specht module. The second conjunct (irreducibility of $S^\lambda$) is a standard fact the source uses implicitly.
• $n>0$ and $n\ne2,4,9$ match the source; $n=1$ is trivial.
• Needed infrastructure: Specht module theory (irreducibility, completeness), characters and Murnaghan–Nakayama, Littlewood–Richardson branching, verified computation for $n\le 64$. The Specht and Kronecker layer is shared with the companion Saxl mission.

Selected references

• I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
• G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
• C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
• S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
• C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
• X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
• N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
• E. Letellier, Tensor products of unipotent characters of general linear groups over finite fields, Transform. Groups 18 (2013), 233–262. https://doi.org/10.1007/s00031-013-9211-3
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf
• OpenAI, Universal Tensor Squares for Symmetric Groups, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-Tensor-Squares-for-Symmetric-Groups-September-24-2026/main.pdf

Motivation

The Ramsey number $R(H,J)$ is the least $N$ such that every red–blue colouring of the edges of $K_N$ contains a red copy of $H$ or a blue copy of $J$. For a cycle $C_m$ against a clique $K_n$ there is a simple lower-bound construction: take $n-1$ disjoint red cliques of order $m-1$ with all edges between them blue. It has $(m-1)(n-1)$ vertices, no red $C_m$ (each red component is too small) and no blue $K_n$ (a blue clique meets each red clique at most once). In 1978 Erdős, Faudree, Rousseau and Schelp conjectured that this construction is optimal whenever $m\ge n\ge3$, apart from $R(C_3,K_3)=6$. Cycle–complete Ramsey numbers are among the few families where exact values are expected over a whole parameter range, and the conjecture has been attacked case by case for decades.

This mission asks for a formal proof of the full conjecture as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open. Part of the proof is a finite case analysis of 3,099 parameter-pattern instances carried out by two exact programs that accompany the paper.

Background

• 1971 — Chartrand and Schuster settle $n=3$ (Bull. AMS 1971).
• 1973 — Bondy and Erdős prove the formula for $m\ge n^2-2$ (JCTB 1973).
• 1978 — Erdős, Faudree, Rousseau and Schelp state the conjecture (J. Graph Theory 1978).
• 1999–2008 — The full range for $n=4$ (Yang–Huang–Zhang, Australas. J. Combin. 1999), $n=5$ (Bollobás et al., Australas. J. Combin. 2000), $n=6$ (Schiermeyer, JGT 2003), $n=7$ (Chen–Cheng–Zhang, Eur. J. Combin. 2008).
• 2005 — Nikiforov proves the formula for $n\ge4$, $m\ge4n+2$ (CPC 2005).
• 2007–2023 — Partial results for $n=8$, including $R(C_8,K_8)$ (Discrete Math. 2009) and $R(C_9,K_8)$ (ISRN Algebra 2011).
• 2021 — Keevash, Long and Skokan prove the formula for $m\ge C\log n/\log\log n$, leaving finitely many open pairs (IMRN 2021).
• September 2026 — The OpenAI preprint claims all remaining pairs (Theorem 1.1, p. 2).

Setting

All graphs are finite and simple. $C_m$ is the cycle on exactly $m$ vertices and $K_n$ the complete graph on $n$ vertices. Identify a red–blue colouring of $K_N$ with its red graph $G$ on $N$ vertices; the blue graph is the complement $\overline G$. A copy of $H$ in $G$ is an injective homomorphism $H\to G$ (copies need not be induced). The Ramsey property $\mathcal R(m,n,N)$ says: every graph $G$ on $N$ vertices contains $C_m$ or its complement contains $K_n$. Then

$$R(C_m,K_n)=\min\{N:\ \mathcal R(m,n,N)\}.$$

Formalization targets

Goal: Theorem 1.1 (p. 2)

For all integers $m\ge n\ge 3$ with $(m,n)\ne(3,3)$,

$$R(C_m,K_n)=(m-1)(n-1)+1,$$

and $R(C_3,K_3)=6$.

Significance

The result itself. It completes a programme that over five decades settled the conjecture for $n\le7$, for long cycles, and for all sufficiently large $n$ by Keevash–Long–Skokan; the preprint's contribution is the remaining finite but large set of pairs. Since Keevash–Long–Skokan's constant is not explicit, the preprint gives a structural reduction that does not need a numerical value of it.

Formalizing it. The statement uses only Mathlib's cycleGraph, complete graphs, complements and subgraph containment. A formal proof would have to certify both the structural lemmas (independent-set expansion, a large-clique lemma, optimal path systems) and the finite verification of 3,099 pattern instances, which the preprint currently delegates to two programs with deduction traces. Bringing such a computation inside a proof assistant is itself a worthwhile contribution. Neither $R(C_m,K_n)$ for general parameters nor any of the previously known infinite families has a machine-checked proof.

Difficulty

The lower bound is the explicit construction above; the work is the upper bound for exact cycle length $m$. Methods that find long cycles (Pósa rotation, Chvátal–Erdős) produce cycles of length at least $m$, not exactly $m$, and forbidding exactly one cycle length gives weak structural information. The preprint passes to a minimal counterexample with independent-set expansion (Lemma 2.2, p. 4), finds a clique of order $\max\{3,\lfloor k/2\rfloor\}$ with $k=m-1$ (Theorem 3.1, p. 5), and optimizes systems of paths through that clique so that every improvement would close a cycle of order exactly $m$. Cliques of order $t\ge9$ are excluded by hand (Proposition 8.4, p. 24); the remaining $3\le t\le8$, $5\le k\le17$ need the finite verification of Section 9 (Proposition 9.1, p. 26).

Formalization scope

• RamseyProperty m n N: for every G : SimpleGraph (Fin N), cycleGraph m ⊑ G or (⊤ : SimpleGraph (Fin n)) ⊑ Gᶜ, where ⊑ is Mathlib's subgraph containment (injective homomorphism, non-induced).
• cycleCliqueRamsey m n = sInf {N | RamseyProperty m n N} in ℕ. If the set were empty, sInf would return 0; the goal's equalities exclude that, so a proof must exhibit the Ramsey property.
• The goal quantifies over integers $m,n$ with $3\le n\le m$, $(m,n)\ne(3,3)$, converting with toNat (harmless since both are at least $3$), and separately states cycleCliqueRamsey 3 3 = 6.
• cycleGraph m on Fin m is the $m$-cycle for $m\ge3$.

Welcome contributions: a verified checker for the pattern enumeration of Section 9, and the classical small cases ($n=3$, Bondy–Erdős for $m\ge n^2-2$).

Selected references

• OpenAI, Cycle–clique Ramsey numbers, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Cycle-clique-Ramsey-numbers-September-25-2026/Cycle-clique-Ramsey-numbers-September-25-2026.pdf
• P. Erdős, R. J. Faudree, C. C. Rousseau, R. H. Schelp, On cycle–complete graph Ramsey numbers, J. Graph Theory 2 (1978). https://doi.org/10.1002/jgt.3190020107
• J. A. Bondy, P. Erdős, Ramsey numbers for cycles in graphs, J. Combin. Theory Ser. B (1973). https://doi.org/10.1016/S0095-8956(73)80005-X
• G. Chartrand, S. Schuster, On the existence of specified cycles in complementary graphs, Bull. Amer. Math. Soc. (1971). https://doi.org/10.1090/S0002-9904-1971-12832-X
• I. Schiermeyer, All cycle-complete graph Ramsey numbers r(C_m,K_6), J. Graph Theory (2003). https://doi.org/10.1002/jgt.10145
• V. Nikiforov, The cycle-complete graph Ramsey numbers, Combin. Probab. Comput. (2005). https://doi.org/10.1017/S096354830400642X
• Y. Chen, T. C. E. Cheng, Y. Zhang, The Ramsey numbers R(C_m,K_7) and R(C_7,K_8), European J. Combin. (2008). https://doi.org/10.1016/j.ejc.2007.05.007
• P. Keevash, E. Long, J. Skokan, Cycle-complete Ramsey numbers, Int. Math. Res. Not. (2021). https://doi.org/10.1093/imrn/rnz119
• V. Chvátal, P. Erdős, A note on Hamiltonian circuits, Discrete Math. (1972). https://doi.org/10.1016/0012-365X(72)90079-9