No problem in mathematics carries more weight than the Riemann hypothesis. In his single eight-page paper of 1859, 'On the Number of Primes Less Than a Given Magnitude,' Bernhard Riemann linked the seemingly erratic distribution of the primes to the zeros of the analytic continuation of the zeta function ζ(s), and conjectured that every nontrivial zero lies exactly on the critical line where the real part equals 1/2. The truth of this statement would pin down the error term in the prime number theorem and tame the fluctuations of the primes around their expected count, and hundreds of theorems already stand proven only 'conditional on RH,' waiting for it to be settled. David Hilbert placed it in his eighth problem in 1900, alongside Goldbach and the twin primes; in 2000 the Clay Mathematics Institute named it one of the seven Millennium Prize Problems, with a million-dollar reward. G. H. Hardy proved in 1914 that infinitely many zeros lie on the critical line, and trillions more have since been verified by computation to do so — overwhelming evidence that is nonetheless not a proof. After more than 160 years it remains unresolved. This mission takes Mathlib's own definition of the hypothesis as its target.

Motivation

A loss network accepts a request only when all resources needed by that request are available. An accepted telephone call, for example, occupies circuits on several links at once. A blocked request leaves immediately. Resource sharing makes route occupancies dependent, even when the arrival streams are independent. For a large network, its exact equilibrium probabilities may be easy to describe but expensive to evaluate. A limit theorem gives a tractable description of fluctuations around the network's typical occupancy. This mission concerns the fixed-topology, growing-capacity regime in Chapter 3 of Kelly and Yudovina, Stochastic Networks, using the supplied Lecture Notes PDF.

The question is not only where mean occupancy settles. Capacity constraints can remove fluctuation directions altogether. The target identifies the surviving Gaussian distribution and retains the moment convergence needed to extract mean occupancies from it.

Setting

There are finitely many links, indexed by $j$, and finitely many routes, indexed by $r$. The circuit-requirement matrix $A$ has nonnegative integer entries: a route-$r$ request occupies $A_{jr}$ circuits on link $j$. Independent Poisson streams bring requests at rates $\nu_r$. Holding times are independent exponentials of mean one. An arrival is accepted precisely when the capacities permit its entire resource requirement.

The occupancy vector $n\in\mathbb N^R$ records calls in progress. With capacity vector $C\in\mathbb N^J$, its feasible states are $S(C)=\{n:An\le C\}$. Equation (3.3) gives the product-form law

These are countable occupancy states. The route and link index sets are finite; the occupancy coordinates have no fixed upper bound shared across the scaling sequence.

For network number $N\ge1$, rates and capacities are $\nu(N)$ and $C(N)$. The matrix $A$ stays fixed and has full row rank. Rates and finite-network capacities are positive, and $\nu(N)/N\to\nu>0$, $C(N)/N\to C>0$ coordinatewise. The limiting capacities are real. A blocking vector $B\in[0,1)^J$ determines carried traffic $x_r=\nu_r\prod_j(1-B_j)^{A_{jr}}$. It satisfies $Ax\le C$, with equality wherever $B_j>0$. The limiting data also satisfy strict slack: $(Ax)_j<C_j$ whenever $B_j=0$. These are the standing conditions of §3.5.1 in the source, printed page 62.

Formalization targets

The first milestone supplies the actual normalizing sum in Equation (3.3), its positivity and convergence, detailed balance for the specified loss rates, and the resulting probability measure. It connects the exact law to the published product-form balance theorem without assuming a normalizer.

The second milestone references the complete integer-capacity primal and dual characterization of Theorem 3.10. The continuous mode $x$ uniquely maximizes

Its blocking representation is the one above. A companion theorem extends all clauses to positive real capacities. Lemma 3.13 is the third milestone:

The goal is Theorem 3.14. Center the exact occupancy law at its finite-network continuous mode:

Let $\mathcal B=\{j:B_j>0\}$, let $H=A_{\mathcal B}$, and put $D=\operatorname{diag}(x)$. The target is

where $U$ is the centered Gaussian supported on $Hu=0$. Every mixed moment converges, and consequently $\mathbb E[n_r(N)]/N\to x_r$. All these conclusions, including moments, belong to the printed theorem, page 64.

Significance

The Gaussian limit distinguishes active links from links with spare capacity. Active constraints suppress certain directions, so the limiting covariance can be singular even though all unconstrained coordinate variances are positive. The theorem also justifies passing from the limiting distribution to mean carried traffic; weak convergence alone does not justify that passage.

The published library already contains a proved product-form detailed-balance theorem with an assumed convergent normalizer. It also contains an Open statement of the full integer-capacity primal and dual characterization. Neither is a proof of the Gaussian limit. This mission adds an explicit measure model, a canonical law for null-event Gaussian conditioning, the required normalization obligation, and targets for distribution and moment convergence. The source presents the limit theorem with a sketch; the formal theorem is an unproved target, not a claim that the sketch has already been machine checked.

Difficulty

Local approximations to probability masses do not by themselves control mass escaping to infinity. They also do not establish convergence of unbounded moments. Remarks 3.15 and 3.16 in the source, pages 64–65, explicitly leave tail estimates out of the sketch. The formal goal retains those obligations without assuming tightness or uniform integrability. This omission is recorded as finding F3.

Another difficulty is that the event $Hu=0$ generally has probability zero under the independent Gaussian law. Ordinary division by its event probability does not define the intended distribution. Strict slack is substantive as well: at a critically loaded one-link system, removing it would incorrectly predict an unconstrained normal limit for fluctuations that are always nonpositive, as recorded in F1.

Formalization scope

Lean uses finite link and route indices, natural matrix entries and finite-network capacities, real rates, and the full countable occupancy space. It reuses the published loss-state and weight definitions. The product measure of real Gaussians is mapped by the explicit residual $z\mapsto z-DH^{\mathsf T}(HDH^{\mathsf T})^{-1}Hz$. Thus the limiting covariance and support are fixed by the data. Empty active sets retain the independent Gaussian; full active rank may give a point mass. Network zero is outside the positive-data assumptions and has no effect on the limits.

Weak convergence is expressed through every bounded continuous real test function. Moments use every multi-index of natural powers, with integrability stated in the conclusion. The blocking selector is computed from the equations, with a zero fallback outside their domain of existence. Existence under positive real capacities remains a theorem obligation. No stochastic limit, moment bound, or convergence premise is hidden in that definition. In particular, a balance identity, an arbitrary proposed limit law, or convergence of means alone cannot satisfy this goal.

No selected statement contains an $O(\cdot)$ estimate or an unspecified failure probability, so there are no explicit-constant replacements. The sketch's unnumbered remainder estimates are not additional targets. Finite-network positivity is the standing domain in which the source defines $B(N)\in[0,1)^J$; no strict slack is imposed on individual finite networks.

Beyond the paper. One strengthened companion extends Theorem 3.10 from positive natural to positive real capacities while retaining every conclusion. Finding F5 records that the source's dual argument uses positivity, not integrality. The faithful integer-capacity item stays referenced as a milestone. No sharpness probe or variant of a proof gap is posed. The strengthened statement supplies the real-capacity bridge needed by the limiting regime.

Selected references

• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. DOI. Citations and numbering here refer to the supplied Lecture Notes on Stochastic Networks PDF, Chapter 3, printed pages 49–81 (PDF pages 57–89), SHA-256 ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a. Equivalence to a particular published printing has not been established.
• F. P. Kelly, “Loss networks,” Annals of Applied Probability 1(3), 319–378, 1991. DOI. The existing Open library item for its Theorem 2.8 supplies the matching integer-capacity characterization referenced by this mission.

Motivation

John Conway asked whether a graph on 99 vertices can have every edge in exactly one triangle and every nonedge in exactly one quadrilateral. He included this question among his five $1,000 problems and explicitly accepted either a construction or a proof of impossibility (Conway, 2017). This mission organizes structural constraints and graph reconstruction around the existing public formal statement, which remains open. It complements the existing Conway mission: both point to the same mathematical question, while this mission curates additional published intermediate theorems and the precise bridges still needed to use them.

The historical restriction most relevant here is Wilbrink's 1984 theorem that a hypothetical graph cannot be vertex-transitive (Wilbrink's paper). That result is already formalized on Prove2Me. The consolidated local Conway99 development also contains graph-owned point, finite-field, and rooted constraints. Its written and finite-check results have different verification levels; the platform-accepted lemmas cited below are the machine-checked part of that work.

Setting

A strongly regular graph with parameters $(n,k,\lambda,\mu)$ is a finite simple graph on $n$ vertices in which each vertex has $k$ neighbours, adjacent vertices have exactly $\lambda$ common neighbours, and distinct nonadjacent vertices have exactly $\mu$ common neighbours. Write $G$ for a candidate graph and $A$ for its integer adjacency matrix, whose $(u,v)$ entry is $1$ when $u$ and $v$ are adjacent and $0$ otherwise. Let $I$ be the identity matrix and $J$ the all-ones matrix. In this mission, the parameter tuple is $(99,14,1,2)$.

The condition $\lambda=1$ makes each edge part of a unique triangle. Each vertex's 14 neighbours split into seven paired edges. The condition $\mu=2$ makes each nonadjacent pair have exactly two common neighbours. These facts lead to $231$ triangles and the matrix equation $A^2+A=12I+2J$, both already proved on the platform (triangle count, matrix identity). Choosing one vertex as a root splits the remaining vertices into its 14 neighbours and 84 nonneighbours; the graph's actual adjacency blocks then satisfy further identities (rooted theorem). The word actual matters: arbitrary matrices satisfying some of these identities have not thereby been shown to arise from one graph.

Formalization targets

Goal

This is the already published Conway99.conway_99 theorem, reused as the goal. A graph satisfying it proves existence; a proof of the negation of this full existential settles nonexistence. Neither outcome has been established in the archive.

Structural and reconstruction targets

The first layer collects necessary facts about every hypothetical $G$: rooted block equations, point-Gram identities, and finite-field identities. The accepted theorems are rooted blocks, point Gram, and finite fields. An independent binary cut-response rank theorem supplies reusable seven-vertex algebra; its statement does not assume a Conway graph. A selected twelve-owner contact theorem gives a further conclusion only when its chosen triangle, owner set, and regularity premises hold.

The reconstruction layer asks whether compatible local data can be obtained from, or assembled into, one graph satisfying all four strongly regular parameters. The public adjacency-matrix formulation and triangle line-system formulation are still open. A future coclique-completion equivalence concerns graphs with a specified independent 22-set; it cannot replace the unrestricted goal unless that set is shown to exist in every candidate. No unpublished or pending statement is presented as a completed milestone.

An accepted admitted-coclique spike theorem supplies a precise lattice membership identity when a 22-point set and its point-vector average are already admitted to one lattice. It does not produce that coclique, establish the needed lattice for every graph, or close the reconstruction gap. An accepted printed-census correction is retained as a reference to prevent the known erroneous expressions from being reused as graph counts; it is an audit of formulas, not a structural exclusion.

Significance

A construction would settle Conway's existence question with a checkable 99-vertex object. A nonexistence proof would explain why the local triangle and common-neighbour conditions cannot coexist globally, despite the standard parameter equations being consistent. Either result must address the whole graph, not one selected root, lattice, shell, or completion packet (Conway's question; formal goal).

The formalization already gives reusable graph-owned interfaces: block identities from an actual root, a point Gram representation, and modular restrictions. Those are machine-checked necessary conditions, while deeper rank, lattice, triangle-transport, and finite-support exclusions in the consolidated local development remain written or locally checked mathematics. This mission makes their status visible and provides a place to connect faithful formal versions as they are published. A conditional theorem remains useful, but its hypotheses must be derived from the candidate graph before it can narrow the unrestricted goal.

Difficulty

The adjacency equation and its eigenvalue multiplicities constrain every candidate but do not determine the binary off-diagonal entries of $A$. Local equations can have feasible matrix or incidence data even when those data have not been embedded in a common simple graph. Conversely, excluding a fixed support, one lattice choice, or a branch with an ordinary point leaves other configurations untouched. The consolidated local frontier records those coverage gaps, including exceptional-only configurations and unexcluded incidence systems. The central task is to close a graph-wide bridge or exhibit a graph, while retaining every hypothesis on narrower results.

Formalization scope

The goal uses Mathlib's SimpleGraph.IsSRGWith and quantifies over a finite vertex type, a graph, and decidable adjacency exactly as in the published statement. Supporting statements may use Fin 99 after an explicit relabelling, integer adjacency matrices, finite triangle sets, real Gram matrices, and finite-field reductions. They must derive data from one G, or mark any independent packet as an additional hypothesis. A theorem about selected owners, a prescribed coclique, a particular determinant or rank, or a saved finite support must keep that restriction visible; none may silently assert that every candidate supplies it.

Existing published definitions and theorems should be imported by their platform IDs. Contributions are welcome for exact bridges between graph, matrix, triangle, and coclique representations; proofs that a conditional packet follows from every candidate; faithful formalizations of written universal constraints; and a construction or unconditional contradiction. The mission's published milestones record actual theorem statements. Prospective bridge descriptions remain research targets until they have separately audited and published platform IDs.

Selected references

• J. H. Conway, Five $1,000 Problems (Update 2017), OEIS attachment, 2017. PDF.
• H. A. Wilbrink, On the (99,14,1,2) strongly regular graph, in Papers Dedicated to J. J. Seidel, EUT-Report 84-WSK-03, Technische Hogeschool Eindhoven, 1984, pp. 342–355. Institutional PDF; publication record.

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$. Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ($L_\infty$) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$.

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

• 1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$.
• 1984. Megiddo extends the method to every fixed $d$, with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
• 1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$. Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
• 1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$. An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$, and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$. Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$. It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$, then $A$ row by row, then $b$. A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$, answers whether $a^Tx^*<b$, $=b$ or $>b$. Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$, the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

1. One query settles half of $n$ hyperplanes on the line ($A(1)=1$, $B(1)=\tfrac12$).
2. $v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$, so there is a basis in which all $a_{ij}\ne0$.
3. For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$, $H_k$.
4. A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$, and the middle hyperplane settles one of them.
5. Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
6. $C(d)\log n$ queries settle all $n$ hyperplanes.
7. If a hyperplane contains no optimal point, all optimal points lie on one side of it.
8. The oracle, Case I: at an optimum relative to $\{x_d=0\}$, two auxiliary systems decide the side or certify global optimality.
9. The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$, systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$, so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$, including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$. The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$, when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

• Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
• Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$. The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$. The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
• Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
• Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$. A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
• Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
• Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$, where the page's last sentence says $\{x_d<0\}$. The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$, the hypothesis its argument uses, since linear independence alone does not give it.
• Not included. Approach II and its bound $O(n(\log n)^{d^2})$, the remarks on slowly growing $d$, the randomized variants, and the applications of §1.
• Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
• N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
• M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
• K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
• R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
• B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

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

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

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

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)

1. Erdős 1947: $R(k)>2^{k/2}$ for all $k\ge 3$.
2. Spencer 1975: for every $\varepsilon>0$, eventually $R(k)\ge(1-\varepsilon)\frac{\sqrt2}{e}\,k\,2^{k/2}$.
3. Erdős–Szekeres 1935: $R(k)\le\binom{2k-2}{k-1}$ for all $k\ge1$.
4. Campos–Griffiths–Morris–Sahasrabudhe 2023: there is $\varepsilon>0$ with $R(k)\le(4-\varepsilon)^k$ for all sufficiently large $k$.
5. 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

Motivation

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

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

Timeline.

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

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

Setting

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

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

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

Formalization targets

Goal (Erdős Problem #30)

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

Milestones (known results, weakest to strongest)

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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)

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

1. Erdős–Rado upper bound: $f(n,k) \le (k-1)^n\, n! + 1$ for $n \ge 1$, $k \ge 2$.
2. Erdős–Rado lower bound: $(k-1)^n < f(n,k)$ for $n \ge 1$, $k \ge 2$.
3. 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$.
4. 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

Motivation

Dirac showed in 1931 that quantum mechanics permits isolated magnetic charges provided electric charge is quantized, but in Maxwell's theory such a magnetic monopole is a point singularity attached to an unobservable "Dirac string". In 1974 G. 't Hooft and, independently, A. M. Polyakov observed that in gauge theories where the electromagnetic group $U(1)$ sits inside a larger group with compact covering group, monopoles arise instead as smooth, finite-energy solutions of the classical field equations, with no singularity and no string. 't Hooft's paper (Nucl. Phys. B79 (1974) 276) does this for the SO(3) model of Georgi and Glashow and computes the mass numerically. The resulting "'t Hooft–Polyakov monopole" became the model example of a topological soliton in gauge theory.

Timeline. 1931: Dirac's quantization argument (Proc. R. Soc. A 133, 60). 1972: Georgi–Glashow SO(3) electroweak model (PRL 28, 1494). 1974: 't Hooft and Polyakov (JETP Lett. 20, 194) describe the regular monopole, 't Hooft by a spherically symmetric ansatz, a reduced one-dimensional energy functional and a numerical minimisation. 1975: Prasad and Sommerfield find a closed-form solution in the limit $\lambda \to 0$ (PRL 35, 760). For $\lambda > 0$ no closed form is known.

Setting

Space and isospin space are both $\mathbb R^3$. A static configuration in the gauge $W_4 = 0$ consists of a Higgs triplet $Q_a(x)$ and a gauge field $W^a_i(x)$, $i, a \in \{1,2,3\}$. With coupling $e$, Higgs self-coupling $\lambda$ and vacuum value $F$ (eqs. (2.1)–(2.3), with $\mu^2 = -\tfrac12\lambda F^2$),

and the static energy is

The vector masses are $M_W = eF$ and the Higgs mass is $M_H = \sqrt\lambda F$. A static solution is a smooth configuration of finite energy at which $E$ is stationary under all compactly supported smooth variations. 't Hooft's gauge-invariant electromagnetic tensor (2.17) is

The spherically symmetric ansatz (2.8) is $Q_a(x) = x_aQ(r)$, $W^a_i(x) = \varepsilon_{iab}x_bW(r)$ with $r = |x|$. The monopole boundary condition is $Q_a(x) \to F x_a/r$ as $r \to \infty$ (eqs. (2.6), (2.11)).

Formalization targets

Goal (Sect. 2 and abstract)

For all $e > 0$, $\lambda > 0$, $F > 0$ there are radial profiles $Q(r), W(r)$ such that the configuration (2.8) is a smooth finite-energy static solution with

i.e. a regular magnetic monopole whose far field is (2.20).

Milestones

1. Eq. (1.5): $\Omega\Omega^\dagger = 1$ for the SU(2) matrix (1.4).
2. Eq. (2.6): the adjoint action of $\Omega$ sends the isovector $(0,0,1)$ to a unit radial isovector.
3. Sect. 2: the boundary condition forces the Higgs field to vanish somewhere.
4. Eq. (2.9): reduced energy density of the ansatz.
5. Eq. (2.13): the Lagrange equation for $W$.
6. Eqs. (2.14)–(2.15): the only power law $W = ar^{-n}$ compatible with (2.13) and $Q = F/r$ is $n = 2$, $a = -1/e$.
7. Eqs. (2.18)–(2.20): the asymptotic fields have $D_iQ_a = 0$ and $F_{ij} = -\varepsilon_{ija}x_a/(er^3)$.
8. Eq. (2.21): total magnetic flux of magnitude $4\pi/e$.
9. Eq. (3.2): the energy in the dimensionless variables $x = eFr$, $\beta = \lambda/e^2$.

Significance

The existence of a regular monopole is what makes the monopole a particle of the theory: its mass $M_m = \frac{4\pi}{e^2}M_WC(\beta)$ (eq. (3.3)) is finite and calculable, and its magnetic charge is fixed by topology rather than put in by hand. The ingredients (hedgehog ansatz, the zero of the Higgs field forced by the boundary condition, the reduction to an ODE system, the gauge-invariant electromagnetic tensor) are reused throughout the theory of solitons in gauge theories.

The result is established in the physics literature; 't Hooft's own argument is partly numerical (trial functions). The mission asks for a machine-checked development: the algebraic and calculus identities of Sects. 1–3, the topological zero, and a complete existence proof for the spherically symmetric solution for every $\lambda > 0$. No machine-checked proof of any of these is known to the proposer.

Difficulty

The identities (milestones 1, 4, 6–9) are finite computations, but milestones 4, 5 and 9 must go through Fréchet derivatives of vector fields on $\mathbb R^3$ and spherical coordinates, where most of the work lies. Milestone 3 is a degree-theoretic statement not available off the shelf. The goal needs an actual existence theorem for a nonlinear coupled ODE system on $(0,\infty)$ with singular coefficients at $r = 0$ and boundary conditions at both ends, followed by regularity of the resulting fields at the origin and the passage from the reduced (radial) equations to the full field equations. 't Hooft's numerical minimisation over trial functions gives no proof that a minimiser exists or is smooth.

Formalization scope

$\mathbb R^3$ is EuclideanSpace ℝ (Fin 3) with Lebesgue measure; indices run over Fin 3 = {0,1,2}, the Levi-Civita symbol is an explicit formula, partial derivatives are Fréchet derivatives in coordinate directions. Fields are static and in the gauge $W_4 = 0$, where the Gauss-law equation holds automatically, so "static solution" means: $C^\infty$ fields, integrable energy density, and zero derivative of the energy along every smooth compactly supported variation of $Q$ and $W_i$. Lean's total operations are used: division by zero is $0$ and the Bochner integral of a non-integrable function is $0$; every statement using them either excludes the degenerate input or is insensitive to it (the goal demands integrability explicitly). The constant $\tfrac18\lambda F^4$ is included so the vacuum has zero energy, as in (2.9).

Two deviations from the printed text, both flagged in the milestones: (i) with standard Pauli matrices, $\Omega\sigma_3\Omega^\dagger$ is $(\sin\theta\sin\varphi,\ \sin\theta\cos\varphi,\ \cos\theta)\cdot\vec\sigma$, whereas (2.6) prints $(\sin\theta\cos\varphi,\ \sin\theta\sin\varphi,\ \cos\theta)$; the milestone states the computed identity. (ii) With $B_k = \tfrac12\varepsilon_{kij}F_{ij}$, (2.20) gives $B = -x/(er^3)$ while (2.21) prints $+x/(er^3)$; the flux milestone therefore states the magnitude $4\pi/e$, and the sign is fixed by (2.20). The asymptotic analysis (2.14)–(2.15) is formalized as an exact statement about pure power laws. The numerical values of $C(\beta)$ in (3.3) are not formalized.

A trivializing reading of the goal is ruled out: the solution must satisfy the non-trivial boundary condition, which by milestone 3 excludes the vacuum, and the stationarity must hold for all variations, not only spherically symmetric ones.

Useful reusable infrastructure: spherical-coordinate integration of radial functions on $\mathbb R^3$, calculus of hedgehog fields, and a Brouwer-degree / no-retraction argument for maps of the sphere. Contributions of any milestone, and of alternative existence proofs (variational, shooting), are welcome.

Selected references

• G. 't Hooft, Magnetic monopoles in unified gauge theories, Nucl. Phys. B79 (1974) 276–284. https://doi.org/10.1016/0550-3213(74)90486-6
• A. M. Polyakov, Particle spectrum in quantum field theory, JETP Lett. 20 (1974) 194.
• P. A. M. Dirac, Quantised singularities in the electromagnetic field, Proc. R. Soc. A 133 (1931) 60. https://doi.org/10.1098/rspa.1931.0130
• H. Georgi, S. L. Glashow, Unified weak and electromagnetic interactions without neutral currents, Phys. Rev. Lett. 28 (1972) 1494. https://doi.org/10.1103/PhysRevLett.28.1494
• M. K. Prasad, C. M. Sommerfield, Exact classical solution for the 't Hooft monopole and the Julia–Zee dyon, Phys. Rev. Lett. 35 (1975) 760. https://doi.org/10.1103/PhysRevLett.35.760

Motivation

Erdős asked, repeatedly and with a rising price tag, for an asymptotic formula for the largest subset of $\{1,\dots,N\}$ that contains no arithmetic progression of a given length. He offered 1000 dollars for it in [Er97c] and 10000 dollars in [Er81, p.4], where he called the question "probably enormously difficult"; elsewhere he described it as "probably unattackable at present". Most of modern additive combinatorics — the density increment method, the triangle removal lemma, Gowers uniformity norms, the arithmetic regularity lemma — grew out of attempts on this single question, and the answer is still unknown, even in the first non-trivial case $k=3$.

Timeline.

• 1936: Erdős and Turán conjecture that $r_k(N)=o(N)$ for every $k$.
• 1946: Behrend constructs large progression-free sets, giving $r_3(N)\ge N\exp(-c\sqrt{\log N})$.
• 1953: Roth proves $r_3(N)=o(N)$, with the quantitative form $r_3(N)\ll N/\log\log N$.
• 1961: Rankin generalises Behrend, giving $r_k(N)\ge N\exp(-c_k(\log N)^{1/(k-1)})$.
• 1969, 1975: Szemerédi proves $r_4(N)=o(N)$ and then $r_k(N)=o(N)$ for all $k$, settling Erdős–Turán.
• 1977: Furstenberg reproves Szemerédi's theorem ergodically, with no effective bound.
• 1998, 2001: Gowers introduces uniformity norms and obtains $r_k(N)\ll N(\log\log N)^{-c_k}$, the first effective bound for general $k$.
• 2017: Green and Tao obtain $r_4(N)\ll N(\log N)^{-c}$.
• 2020: Bloom and Sisask obtain $r_3(N)\ll N(\log N)^{-1-c}$, the first bound past the $N/\log N$ barrier.
• 2023: Kelley and Meka obtain $r_3(N)\le N\exp(-c(\log N)^{1/12})$.
• 2024: Leng, Sah and Sawhney obtain $r_k(N)\ll N\exp(-(\log\log N)^{c_k})$ for $k\ge5$.

Every upper bound in this list is still astronomically far from Behrend's lower bound, and no candidate asymptotic formula has been proposed for any $k\ge3$.

Setting

Fix an integer $k$. A non-trivial $k$-term arithmetic progression is a list $a,\,a+d,\,a+2d,\dots,a+(k-1)d$ of natural numbers with common difference $d>0$; the requirement $d>0$ is what "non-trivial" means, and it forces the $k$ terms to be distinct. A finite set $A\subseteq\mathbb N$ is $k$-AP-free if it contains no such progression. Write

The mission takes its formal definition of $r_k$ verbatim from the formal-conjectures entry for this problem, so that the goal below is literally the statement recorded there. In that development a set is called free of progressions of length $l$ when every subset of it that is an arithmetic progression of length $l$ forces $l\le1$. Progressions of length $0$ and $1$ count as trivial, so under that convention every set is free of them and $r_0(N)=r_1(N)=N$; the interesting range begins at $k\ge2$. Every statement in this mission that depends on the convention carries an explicit hypothesis on $k$.

On that range, $r_k(N)$ is non-decreasing in both $N$ and $k$, satisfies $r_k(M+N)\le r_k(M)+r_k(N)$, and hence, by Fekete's subadditivity lemma, $r_k(N)/N$ converges. Szemerédi's theorem is the statement that the limit is $0$; the whole difficulty of this mission lies in how fast it goes to $0$.

Formalization targets

Goal

This is erdos_142.variants.lower of the formal-conjectures file for Erdős 142, reproduced binder for binder, over that file's own definition of $r_k$.

The headline theorem in that file, erdos_142, states $r_k(N)=\Theta(f)$ with the comparison function left as an answer(sorry) placeholder, and the same is true of its variants.upper and variants.three. Those are not closed propositions and cannot serve as a mission goal: the literal request of Erdős Problem #142 — "prove an asymptotic formula for $r_k(N)$" — has no known right-hand side for any $k\ge3$, which is exactly why the file leaves a hole there. variants.lower is the one formalizable target in the file, and it is also the strongest precisely-stated form the problem page attaches to #142: Erdős offered 5000 dollars for (essentially) exactly it, as recorded under Erdős Problem #3. It is known for $k=3$ — it follows from Bloom–Sisask 2020, and a fortiori from Kelley–Meka 2023 — trivial for $k=2$, where $r_2(N)=1$, and open for every $k\ge4$. It fixes no constants, so no future improvement can invalidate it.

A weaker open question

Erdős remarked in [Er80, p.92] that even this separation between consecutive progression lengths is not known. Here [Er80] is the erdosproblems.com bibliography key for Erdős's 1980 paper; it is a citation, not a pointer to Erdős Problem #80, which is an unrelated question about books in graphs. This statement has no counterpart in formal-conjectures: the file for #142 contains only the $\Theta$, $o$ and $O$ variants above, and the only two files in that repository that mention $r_k$ at all are the ones for #142 and #139.

Significance

Proving $r_k(N)=o_k(N/\log N)$ for all $k$ yields, by a standard summation argument, Erdős's conjecture that every $A\subseteq\mathbb N$ with $\sum_{a\in A}1/a=\infty$ contains arbitrarily long arithmetic progressions — the 5000-dollar Erdős Problem #3, of which the Green–Tao theorem on primes is the best-known special case. Below that threshold, quantitative bounds on $r_k$ control the density at which progressions must appear in any concrete set, and are the input to results on progressions in the primes, in sumsets, and in sparse random subsets of the integers.

Formalization status is uneven, and this mission is designed around that gap. Mathlib already contains the $k=3$ theory in a usable form: the predicate ThreeAPFree, the Roth number rothNumberNat, its subadditivity, and a complete formalization of Behrend's construction (Behrend.roth_lower_bound). Mathlib does not contain Roth's theorem, Szemerédi's theorem, or any of the modern upper bounds; to the best of current knowledge none of Roth, Szemerédi, Gowers, Green–Tao, Kelley–Meka or Leng–Sah–Sawhney has a machine-checked proof anywhere. The formal-conjectures entry states the problem but proves nothing: every declaration in it is a sorry. Two of this mission's targets are taken from that repository — the goal from its file for #142, and the Szemerédi milestone from its file for #139, which uses the same $r_k$; those are the only two files there that mention $r_k$. The milestones therefore split cleanly: the first six are reachable now on top of Mathlib, and the last five are open formalization projects of independent value.

Difficulty

Every known upper bound for $r_k$ runs a density increment: if $A\subseteq\{1,\dots,N\}$ of density $\delta$ has no $k$-term progression, find a long subprogression on which $A$ has density $\delta(1+c(\delta))$, and iterate. The bound this produces is governed entirely by two quantities — how large the increment $c(\delta)$ is, and how much of the interval survives one step. For $k\ge4$ the increment is extracted from an inverse theorem for the Gowers $U^{k-1}$-norm, and the best available correlation bounds there are quasipolynomial in $\delta$; iterating a quasipolynomial increment cannot do better than $N\exp(-(\log\log N)^{c})$, which is nowhere near $N/\log N$. Reaching $N/\log N$ requires an increment with polynomial dependence on $\delta$ together with a subprogression of polynomial length, and that combination is currently available only for $k=3$, through the sifting and almost-periodicity machinery of Kelley–Meka. No soft or averaging argument can substitute: Behrend's construction shows the truth at $k=3$ is $N\exp(-\Theta(\sqrt{\log N}))$, so the answer is not a power of $\log N$ and cannot be produced by any argument whose output has that shape.

Formalization scope

The mission's definition file Erdos142Basic carries two layers, and every statement in the mission is written against them.

1. The source definitions, ported verbatim. IsAPOfLengthWith, IsAPOfLength, IsAPOfLengthFree and r are the declarations of the formal-conjectures entry, transcribed unchanged into the mission's namespace: a set is an arithmetic progression of length $l$ with first term $a$ and difference $d$ when it has exactly $l$ elements and equals $\{a+nd : n<l\}$; it is free of length-$l$ progressions when every progression of length $l$ inside it forces $l\le1$; and $r_k(N)$ is the supremum of $|S|$ over subsets $S\subseteq\{1,\dots,N\}$ free of length-$k$ progressions. The ground set is Finset.Icc 1 N, and the supremum is sSup over $\mathbb N$; the file proves the two facts that make it a genuine maximum (le_r and r_le).

2. An elementary handle. HasAP k A is ∃ a d, 0 < d ∧ ∀ i < k, a + i * d ∈ A, and APFree k A its negation. This form carries no cardinality side condition in $\mathbb N\cup\{\infty\}$ and is what a solver actually wants to induct on. The first milestone is exactly the bridge between the two layers.