All missions

Motivation

A divergent reciprocal sum is a sparse largeness condition on integers. The mission asks whether it still forces additive structure of every finite length. The source manuscript presents the surrounding research claim.

Setting

For A⊆ℕ, reciprocalTerm(A,n) is 1/n when n∈A and zero otherwise, using Lean’s total real inverse at n=0. A nonconstant arithmetic progression has terms a+i·d with positive integer d.

Formalization target

Prove

$$\sum_{n\in A}\frac1n\text{ is not summable}\quad\Longrightarrow\quad\forall k\in\mathbb N,\ \exists a\in\mathbb N,\ d\in\mathbb N_{>0},\quad a+id\in A\ (i<k).$$

The starting term a is a natural number and is not separately required positive; the step d is strictly positive.

The selected formal target is OAI.Erdos3.manuscriptReciprocalProgressionTheorem.

Significance and status

The selected endpoint is the reciprocal-sum progression theorem. The manuscript’s quantitative bounds for progression-free subsets motivate it but are not supplied as separate published targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Positive density arguments alone do not cover all sets with divergent reciprocal sums. The hypothesis permits sets whose density tends to zero.

Formalization scope

The formal hypothesis is ¬Summable of a real sequence and ranges over all natural-number sets. All natural lengths k are included, including the degenerate zero and one cases. The n=0 summand equals zero and does not affect divergence. No quantitative constants are asserted here.

Selected references

• OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

How well can a graph be drawn inside a Banach space without stretching some distances much more than others? The distortion of the best such drawing measures the mismatch between the graph's metric and the geometry of the space. Diamond graphs are a standard test family: each edge is repeatedly replaced by parallel two-edge paths, so the graph contains many "midpoints" between the same two endpoints at every scale. For binary diamonds, bounded distortion in a space is tied to the failure of super-reflexivity (Johnson–Schechtman 2009). For countably branching diamonds, where each edge is replaced by infinitely many paths, the relevant property is asymptotic midpoint uniform convexity (AMUC): an equivalent AMUC norm prevents uniform embeddings (Baudier et al. 2017).

This mission asks for an explicit, quantitative lower bound on the distortion of countably branching diamonds in two specific James-type tree spaces, deduced from a midpoint "lens" estimate for those spaces.

Timeline

• 1974. James introduces the square-sum norm over disjoint tree segments (doi:10.1090/S0002-9904-1974-13580-9).
• 2001. Girardi proves asymptotic uniform convexity of the coordinate predual and dual of the binary James tree space (doi:10.4064/sm147-2-2).
• 2004. Lee and Naor give quantitative lower bounds for binary diamonds in $L_p$, $1<p\le2$, by summing a convexity inequality over levels (doi:10.1007/s00039-004-0473-8).
• 2009. Johnson and Schechtman characterize super-reflexivity by non-embeddability of binary diamonds (doi:10.1142/S1793525309000114).
• 2016. Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov introduce AMUC and characterize it via lenses (doi:10.1016/j.jmaa.2015.11.061).
• 2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang prove that an AMUC renorming with power-type modulus $t^p$ forces distortion $\gtrsim k^{1/p}$ for depth-$k$ countably branching diamonds, and prove a converse under unconditional asymptotic structure (arXiv:1612.01984).
• 2018, 2021. Swift and Perreau extend the converse to bundle graphs and dual settings under additional structure (arXiv:1710.00877, arXiv:2104.10494).
• 2025. Malthaner gives a coloring-based proof of the power-type lower bound (arXiv:2310.03257).

The source of this mission is an OpenAI preprint dated September 27, 2026; its lens input comes from the companion OpenAI preprint Midpoint lenses in segment spaces of the same date.

Setting

Diamonds. The normalized diamond $\mathcal D_0$ is one edge of length $1$. $\mathcal D_{k+1}$ replaces every edge of $\mathcal D_k$ by countably many internally disjoint two-edge paths with the same endpoints, each new edge having half the length of its parent. Let $d_k$ be the shortest-path metric. A map $f:\mathcal D_k\to Y$ has distortion at most $D$ if for some scale $s>0$

$$s\,d_k(u,v)\le\|f(u)-f(v)\|\le D\,s\,d_k(u,v)\qquad(u,v\in\mathcal D_k).$$

Tree spaces. Let $\mathcal T=\coprod_{h\ge1}\mathbb N^{\le h}$ (one rooted tree of each finite height, prefix order inside each tree). A segment is the set of vertices between two comparable nodes. For a finitely supported array $a$,

$$\rho(a)=\sup\Bigl\{\Bigl(\sum_{j=1}^m\Bigl|\sum_{s\in S_j}a_s\Bigr|^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.$$

$J$ is the completion and $X=J^*$ with the dual norm. On $T_\infty=\mathbb N^{<\omega}$ (root included) the same formula defines $J_\infty$, and $B_\infty=\overline{\operatorname{span}}\{e_t^*\}\subset J_\infty^*$ is the closed span of the coordinate functionals.

Formalization targets

Goal: Theorem 1.1

For every $k\ge0$ and every distortion-$D$ embedding of $\mathcal D_k$ into $Y\in\{X,\ B_\infty\}$,

$$D^2\ \ge\ 1+\frac k4.$$

The Lean statement OAI.DiamondDistortion.headline_all_pairs is the conjunction of the two cases. It is open on the platform.

Significance

The bound shows that the countably branching diamonds do not embed with uniformly bounded distortion into either space, with an explicit square-root growth rate. Combined with the companion results that neither space admits an equivalent asymptotically uniformly convex norm, and that the forest dual $X$ is reflexive, it shows that the diamond obstruction can hold in reflexive spaces without AUC renormability, so the unconditional-structure hypotheses in the known converses are doing real work. The constant $1/4$ is obtained by retaining the full quadratic budget of the lens inequality. The paper also gives direct energy proofs (Theorem 5.1, Propositions 4.2–4.3) with weaker constants, and general transfer theorems (Section 7) from lens inequalities to distortion bounds.

The theorem is proved in the OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formalization would certify both the metric deduction and, through its input, the tree-space lens estimate.

Difficulty

The input lens inequality bounds only the tail of a displacement outside a finite head. Turning it into a loss of squared edge stretch at every replacement level requires selecting, among infinitely many middle vertices, two whose head projections nearly coincide, so that their half-difference is a tail vector that still lies in the lens. Doing this simultaneously along a descending chain of edges, with the head growing at each step, and summing the losses without wasting the quadratic budget is where the constant is decided. A binary diamond argument does not transfer, because finitely many midpoints give no near-coincident projections.

Formalization scope

• Diamond.Vertex k and Diamond.Edge k are defined by recursion on the stage, each parent edge receiving new vertices indexed by $\mathbb N$; Diamond.graph k is the undirected replacement graph and Diamond.distance k u v is SimpleGraph.dist divided by $2^k$. Since distortion is scale invariant, the normalization does not affect the statement.
• ForestDual is the full continuous dual of the completion of the finite-height forest James space; InfinitePredual is the norm-closed span of coordinate functionals in the dual of the infinite-tree space, with the subspace norm.
• Segments are nonempty finite intervals of an ancestral partial order; test families are finite and pairwise disjoint.
• The conclusion is stated as $1+k/4\le D^2$, with $s>0$ given and the two-sided bound holding for all pairs $u,v$.

A complete development needs the James segment norm and its dual, coordinate projections onto finite ancestral sets, the companion lens estimate, and graph distances on the countably branching diamonds. This infrastructure is shared with the other missions of this family. Formal proofs of Theorem 7.2 (lens-to-distortion transfer) and Theorem 7.12 (AMUC prevents uniform embeddings) are welcome as reusable components.

Selected references

• OpenAI, Distortion of countably branching diamonds from midpoint and tree energies, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Diamond-distortion-from-midpoint-and-tree-energies-September-27-2026/manuscript.pdf
• OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
• F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• J. R. Lee, A. Naor, Embedding the diamond graph in $L_p$ and dimension reduction in $L_1$, Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0473-8
• W. B. Johnson, G. Schechtman, Diamond graphs and super-reflexivity, J. Topol. Anal., 2009. https://doi.org/10.1142/S1793525309000114
• R. Malthaner, On Matoušek-like embedding obstructions of countably branching graphs, J. Math. Anal. Appl., 2025. https://arxiv.org/abs/2310.03257
• R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
• M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2

Motivation

Bernoulli percolation is the simplest model of a random medium: each edge (or each vertex) of a lattice is independently kept open with probability $p$, and one studies the connected components (clusters) of open edges or vertices. As $p$ increases, an infinite cluster appears at a critical parameter $p_c$. Whether an infinite cluster already exists at $p_c$ decides whether the phase transition is continuous, and it is the basic question about critical behaviour. On the nearest-neighbour cubic lattice $\mathbb Z^3$ it has been a central open problem of probability and statistical physics since the 1980s; the dimensions where it was settled were $d=2$ and sufficiently high $d$.

Timeline

• 1957. Broadbent and Hammersley introduce percolation as a model of transport through a random medium (doi:10.1017/S0305004100032680).
• 1960. Harris proves that there is no infinite cluster at $p=1/2$ for bond percolation on $\mathbb Z^2$ (doi:10.1017/S0305004100034241).
• 1980. Kesten identifies the square-lattice bond threshold as $1/2$, which with Harris's theorem gives critical nonpercolation for planar bonds (doi:10.1007/BF01197577).
• 1981. Russo proves critical nonpercolation for site percolation on the square lattice (doi:10.1007/BF00535742).
• 1990. Hara and Slade establish mean-field critical behaviour, including $\theta(p_c)=0$, in sufficiently high dimension via the lace expansion (doi:10.1007/BF02108785). Grimmett and Marstrand prove that slab thresholds converge to $p_c$ and develop dynamic renormalization (doi:10.1098/rspa.1990.0100).
• 1996. Benjamini and Schramm conjecture that $\theta(p_c)=0$ on every quasi-transitive graph with $p_c<1$ (doi:10.1214/ECP.v1-978).
• 2016. Duminil-Copin, Sidoravicius and Tassion prove critical nonpercolation for bond percolation on slabs $\mathbb Z^2\times\{0,\dots,k\}$ (doi:10.1002/cpa.21641); this does not by itself give the full $\mathbb Z^3$ result.
• 2017. Fitzner and van der Hofstad reach the nearest-neighbour bond range $d\ge 11$ (doi:10.1214/17-EJP56).
• 2020. Heydenreich and Matzke give a detailed site lace-expansion treatment in high dimension (doi:10.1007/s10955-020-02607-y).
• 2024. Kozma and Nitzan reduce $\theta(p_c)=0$ to a conjectured multiplicative gluing inequality (arXiv:2401.12397).
• 2026. Public, non-peer-reviewed announcements report AI-assisted proofs of critical nonpercolation, including a reported Lean formalization for bonds on $\mathbb Z^d$, $d\ge2$ (Leder, August 2026).

The source of this mission is an OpenAI preprint dated September 24, 2026, giving a self-contained argument for both bond and site percolation on $\mathbb Z^3$.

Setting

Vertices are $x\in\mathbb Z^3$; $x$ and $y$ are nearest neighbours if $y=x\pm e_i$ for a coordinate vector $e_i$.

• Bond model. Each edge $\{x,x+e_i\}$ is open independently with probability $p$. Two vertices are connected if an open path joins them (a path of zero edges is allowed).
• Site model. Each vertex is open independently with probability $p$. Two vertices are connected if a nearest-neighbour path joins them with every vertex open, endpoints included; in particular the cluster of a closed vertex is empty.

Let $\mathbb P_p$ be the product law, $\theta(p)=\mathbb P_p(\text{the cluster of }0\text{ is infinite})$, and

$$p_c=\inf\{p\in[0,1]:\theta(p)>0\},$$

defined separately for bonds ($p_c^{\mathrm{bond}}$) and sites ($p_c^{\mathrm{site}}$).

Formalization targets

Goal: Theorem 1.1

$$\mathbb P_{p_c^{\mathrm{bond}}}\bigl(\text{every bond cluster in }\mathbb Z^3\text{ is finite}\bigr)=1,\qquad \mathbb P_{p_c^{\mathrm{site}}}\bigl(\text{every site cluster in }\mathbb Z^3\text{ is finite}\bigr)=1.$$

The Lean statement OAI.CriticalZ3.critical_no_infinite is the conjunction of these two almost-sure statements. It is open on the platform.

Significance

Theorem 1.1 gives continuity of the percolation probability at the transition: $\theta(p)\to0$ as $p\downarrow p_c$ (the paper derives this on p. 1 from the theorem and finite-box approximation). It is the three-dimensional case of the Benjamini–Schramm criticality question and of the classical $\theta(p_c)=0$ problem, which had resisted both planar methods (which rely on duality unavailable in three dimensions) and the lace expansion (which needs high dimension). The site statement is not a formal consequence of the bond statement: site bits become hyperedges with an endpoint convention that must be preserved.

The result is proved in an OpenAI preprint, which has not been peer reviewed. A public announcement reports a Lean formalization of the bond case on $\mathbb Z^d$; no machine-checked proof of this exact statement exists on the platform, and the site case is not covered by that announcement's formalization. A formal proof here would certify both models in one development.

Difficulty

The natural route is renormalization: show that if an infinite cluster exists at $p_c$, then good finite-box events have high probability, persist at some $q<p_c$, and can be glued into an infinite cluster at $q$. The gluing step is where the obvious argument fails. Positive correlation (Harris–FKG) controls the probability that two increasing events both occur, but here one needs the probability of reaching a relay set and then a target, conditioned on an explored region; without a comparison inequality of the form $\mathbb P(o\leftrightarrow A,\ o\leftrightarrow T)\ge \mathbb P(o\leftrightarrow A)\min_{a\in A}\mathbb P(a\leftrightarrow T)$ the losses compound. Slab results do not suffice: extinction at each slab threshold plus convergence of thresholds does not give extinction on $\mathbb Z^3$.

Formalization scope

• Vertex := Fin 3 → ℤ; bonds are pairs (x, i) representing the edge from x to step x i = x + e_i, so each edge appears once.
• bondLaw p and siteLaw p are Measure.infinitePi of bernoulliMeasure true false, giving mass $p$ to "open"; parameter clamps $p$ into $[0,1]$.
• Connectivity is Relation.ReflTransGen of the open-adjacency relation; siteCluster ω x is empty unless ω x = true, matching the endpoint convention.
• bondCritical and siteCritical are sInf of $\{p\in[0,1]:\mathbb P_p(\text{cluster of }0\text{ infinite})>0\}$. The statement does not assume $p_c<1$; it is a known fact for $\mathbb Z^3$, and a solver may need to prove it to rule out the empty-set convention.
• The conclusion quantifies over all vertices: almost surely every cluster is finite.

A complete development needs product Bernoulli measures on countable index sets, monotone coupling, increasing events and Harris–FKG, the finite hyperedge comparison inequality, and a planar boundary-counting lemma. The percolation infrastructure is reusable for the quasi-transitive generalization in the same family. Contributions formalizing Proposition 2.1 (joint connection comparison), Corollary 2.3 (failure comparison), Lemma 4.1 (extension estimate) and Lemma 5.1 (neighbouring-box relay) are welcome.

Selected references

• OpenAI, Critical bond and site percolation on the cubic lattice, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-bond-and-site-percolation-on-the-cubic-lattice-September-24-2026/paper.pdf
• I. Benjamini, O. Schramm, Percolation beyond $\mathbb Z^d$, many questions and a few answers, Electron. Commun. Probab., 1996. https://doi.org/10.1214/ECP.v1-978
• S. R. Broadbent, J. M. Hammersley, Percolation processes. I. Crystals and mazes, Proc. Cambridge Philos. Soc., 1957. https://doi.org/10.1017/S0305004100032680
• T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc., 1960. https://doi.org/10.1017/S0305004100034241
• H. Kesten, The critical probability of bond percolation on the square lattice equals 1/2, Comm. Math. Phys., 1980. https://doi.org/10.1007/BF01197577
• L. Russo, On the critical percolation probabilities, Z. Wahrsch. Verw. Gebiete, 1981. https://doi.org/10.1007/BF00535742
• T. Hara, G. Slade, Mean-field critical behaviour for percolation in high dimensions, Comm. Math. Phys., 1990. https://doi.org/10.1007/BF02108785
• G. R. Grimmett, J. M. Marstrand, The supercritical phase of percolation is well behaved, Proc. R. Soc. Lond. A, 1990. https://doi.org/10.1098/rspa.1990.0100
• H. Duminil-Copin, V. Sidoravicius, V. Tassion, Absence of infinite cluster for critical Bernoulli percolation on slabs, Comm. Pure Appl. Math., 2016. https://doi.org/10.1002/cpa.21641
• R. Fitzner, R. van der Hofstad, Mean-field behavior for nearest-neighbor percolation in d>10, Electron. J. Probab., 2017. https://doi.org/10.1214/17-EJP56
• M. Heydenreich, K. Matzke, Critical site percolation in high dimension, J. Stat. Phys., 2020. https://doi.org/10.1007/s10955-020-02607-y
• G. Kozma, S. Nitzan, A reduction of the θ(p_c)=0 problem to a conjectured inequality, preprint, 2024. https://arxiv.org/abs/2401.12397

Motivation: Saxl's conjecture on the staircase tensor square

The irreducible complex representations of the symmetric group $S_n$ are the Specht modules $S^\lambda$, indexed by partitions $\lambda\vdash n$. How a tensor product $S^\alpha\otimes S^\beta$ (with diagonal action) decomposes is recorded by the Kronecker coefficients

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

for which no positive combinatorial rule is known; even deciding positivity is hard, and the question is studied in algebraic combinatorics and geometric complexity theory. In 2012 Jan Saxl proposed that the staircase $\rho_m=(m,m-1,\dots,1)$, a partition of $N_m=m(m+1)/2$, has a tensor square containing every irreducible representation of $S_{N_m}$.

Timeline

• 2012 — Saxl proposes the conjecture at the UCLA Combinatorics Seminar (20 March 2012), as recorded by Pak, Panova and Vallejo.
• 2010 — Brown, van Willigenburg and Zabrocki show that $S^{(m,m-1)}\otimes S^{(m,m-1)}$ is the multiplicity-free sum of all irreducibles with at most four rows (BWZ 2010, Cor. 4.1).
• 2013 — Heide, Saxl, Tiep and Zalesski prove that the Steinberg square of most finite simple groups of Lie type contains every irreducible, a motivating precedent (HSTZ 2013, Thm 1.2).
• 2015 — Ikenmeyer proves positivity for all $\lambda$ comparable with $\rho_m$ in dominance order, and all hooks (Ikenmeyer 2015).
• 2016 — Pak, Panova and Vallejo formulate the conjecture in print, give a character-nonvanishing criterion, and handle hooks and two-row shapes for large $m$ (PPV 2016).
• 2017 — Luo and Sellke: almost every partition occurs (uniform and Plancherel measures) (Luo–Sellke 2017).
• 2018–2021 — Bessenrodt: double hooks (2018); Bessenrodt, Bowman and Sutton: all 2-height-zero constituents and framed staircases (2021); Li: triple hooks (2021).
• 2023 — Harman and Ryba: the staircase tensor cube contains everything (Harman–Ryba 2023).
• 2025 — Letellier and Nam prove the staircase-square statement for unipotent characters of $\mathrm{GL}_n(q)$, a different character theory (Letellier–Nam 2025).
• 2026 — An OpenAI preprint, A Cyclic Polytabloid Proof of Saxl's Conjecture (OpenAI Math Release, September 24, 2026), claims a proof of the full conjecture. It has not been peer reviewed and the theorem is not formally verified.

Setting

A partition is a Mathlib YoungDiagram. The Lean development builds $S^\lambda$ concretely: for a tableau $t$ (a bijection between $\{0,\dots,n-1\}$ and the cells), the polytabloid $e_t$ is the signed sum over the column group of $t$ of the permuted indicator of the row word of $t$, inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$; Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The coefficient kronecker a b t is the complex dimension of the space of $S_n$-intertwining maps from spechtRep t into spechtRep a ⊗ spechtRep b. The staircase staircase m is the diagram of cells $(i,j)$ with $i+j<m$, i.e. $\rho_m$.

Formalization targets

Goal: Saxl's conjecture

For every integer $m\ge1$ and every partition $\lambda\vdash N_m$,

$$g(\rho_m,\rho_m,\lambda)>0 ,$$

equivalently $S^{\rho_m}\otimes S^{\rho_m}$ contains every irreducible representation of $S_{N_m}$. This is Theorem 1.1 of the source, formalized as SaxlConjecture (positivity of kronecker for every Young diagram $\mu$ with as many cells as staircase m). The goal is published on the platform with status Open.

Significance

The result itself. Saxl's conjecture is the best-known instance of the tensor-square covering problem for symmetric groups. The source proves a stronger cyclic form (its Theorem 3.1): every $S^\lambda$ already occurs in the submodule $W_m$ generated by one explicit tensor $v_{R_m}\otimes v_{C_m}$ of row and column polytabloids. A companion preprint uses this cyclic form to construct, for every $n\notin\{2,4,9\}$, an irreducible representation of $S_n$ whose tensor square contains every irreducible (the tensor square conjecture of Pak–Panova–Vallejo).

Formalizing it. The Lean statement is the classical, non-cyclic conclusion, the form in which the conjecture is usually quoted. A formal proof would require Specht-module theory (irreducibility, Young's rule, branching, induced modules), none of which is presently in Mathlib in usable form; that layer would be reusable across representation theory of $S_n$.

Difficulty

Positivity of a Kronecker coefficient cannot be read off from characters in general: character sums cancel, and the families handled earlier (hooks, two rows, double and triple hooks, dominance-comparable shapes, 2-height-zero shapes) each relied on a special structure. Asymptotic statements (almost all $\lambda$) or higher powers (cube, fourth power) leave exceptional constituents. An induction on $m$ must retain an explicit vector at every step, because knowing that a constituent appears somewhere in a smaller square does not propagate through the projections needed to grow the staircase.

Formalization scope

• staircase m has cells $\{(i,j): i+j<m\}$, with $m(m+1)/2$ cells; canonicalTableau fixes one enumeration of cells (any enumeration gives an isomorphic module). The target diagram ranges over all YoungDiagrams of the same cardinality.
• kronecker is Module.finrank ℂ of Representation.IntertwiningMap, the genuine multiplicity; positivity means a nonzero equivariant map $S^\lambda\to S^{\rho_m}\otimes S^{\rho_m}$ exists.
• The case $m\ge1$ matches the source; $m=0$ is excluded.
• Needed infrastructure: Specht modules and polytabloid bases, Young's rule and dominance, sign twists, induction and restriction, Littlewood–Richardson branching. The definitions are shared verbatim with the companion universal-tensor-square 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
• A. A. H. Brown, S. van Willigenburg and M. Zabrocki, Expressions for Catalan Kronecker products, Pacific J. Math. 248 (2010), 31–48. https://doi.org/10.2140/pjm.2010.248.31
• 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
• C. Bessenrodt, C. Bowman and L. Sutton, Kronecker positivity and 2-modular representation theory, Trans. Amer. Math. Soc. Ser. B 8 (2021), 1024–1055. https://doi.org/10.1090/btran/70
• 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 and G. Nam, The Saxl conjecture and the tensor square of unipotent characters of GL_n(q), Algebr. Comb. 8 (2025), 1119–1140. https://doi.org/10.5802/alco.434
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf

Motivation

A self-similar measure on the line is the natural probability measure on the attractor of finitely many contracting similarities $\varphi_i(x)=r_ix+t_i$, chosen with probabilities $p_i$. Self-similar measures are the basic test case for fractal dimension theory; Bernoulli convolutions, the laws of $\sum_j\pm\lambda^j$, are the classical example. When the pieces $\varphi_i(K)$ are well separated, the dimension is given by the entropy-to-Lyapunov formula $H(p)/\chi$. When they overlap, dimension can drop, and the question is exactly how much. If two compositions of the same length coincide as maps (an exact overlap), information is genuinely lost; the entropy-rate dimension conjecture, formulated in Varjú's survey, predicts that this is the only mechanism: the dimension equals $\min\{1,h_{RW}/\chi\}$, where $h_{RW}$ is the entropy rate of the random walk on composed maps.

This mission asks for a formal proof of that formula, as stated in an OpenAI preprint dated September 24, 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.

Background

• 1946–1981 — Moran (Proc. Camb. Phil. Soc. 1946) and Hutchinson (Indiana 1981) give the similarity-dimension formula under separation and the invariant-measure construction.
• 1939–1996 — Erdős proves singularity of Bernoulli convolutions at reciprocal Pisot parameters (AJM 1939); Garsia introduces the entropy rate (Pacific J. Math. 1963); Solomyak proves a.e. absolute continuity (Annals 1995).
• 2009 — Feng and Hu prove exact dimensionality of self-similar measures without separation (CPAM 2009).
• 2014 — Hochman shows a dimension drop forces superexponential concentration of cylinders (Annals 2014).
• 2019 — Breuillard–Varjú (Ann. Probab. 2019) and Varjú's full dimension for transcendental parameters (Annals 2019).
• 2021 — Baker and Bárány–Käenmäki construct systems without exact overlaps whose cylinders approach superexponentially (Adv. Math. 2021, Adv. Math. 2021).
• 2022–2025 — Rapaport proves the no-exact-overlap formula for algebraic ratios (Ann. Sci. ENS 2022); Rapaport–Varjú treat homogeneous three-map systems (Duke 2024); Feng–Feng treat algebraic translations (J. LMS 2025).
• 2026 — Varjú's survey states the entropy-rate conjecture (Conjecture 3, arXiv:2509.22042).
• September 2026 — The OpenAI preprint claims the conjecture in full (Theorem 1.1, p. 2).

Setting

Let $\Lambda$ be a finite nonempty alphabet and $\varphi_i(x)=r_ix+t_i$ with $0<|r_i|<1$, $t_i\in\mathbb R$; different symbols may give the same map, and ratios may be negative and unequal. Let $p=(p_i)$ be a probability vector with all $p_i>0$. The self-similar measure $\mu$ is the Borel probability measure with

$$\mu=\sum_{i\in\Lambda}p_i\,(\varphi_i)_*\mu .$$

For a word $w=i_1\cdots i_n$ let $\varphi_w=\varphi_{i_1}\circ\cdots\circ\varphi_{i_n}$, and let $G_n$ be the random affine map $\varphi_w$ when the letters are independent with law $p$. With logarithms in base $2$,

$$h_{RW}=\inf_{n\ge1}\frac{H(G_n)}{n},\qquad \chi=-\sum_ip_i\log|r_i|>0,$$

where $H$ is Shannon entropy of the distribution of the map $G_n$ (coinciding words are merged). The lower Hausdorff dimension of $\mu$ is $\dim_H\mu=\inf\{\dim_HE: E\ \text{Borel},\ \mu(E)>0\}$. The system has no exact overlaps if distinct words of the same length give distinct maps.

Formalization targets

Milestone: Corollary 6.3 (p. 20) — dimension of the attractor

If there are no exact overlaps, the attractor $K=\{\lim_n\varphi_{\omega_1}\circ\cdots\circ\varphi_{\omega_n}(0)\}$ is compact and nonempty, the equation $\sum_i|r_i|^s=1$ has a unique solution $s_*\ge0$, and $\dim_HK=\min\{1,s_*\}$.

Milestone: Corollary 6.4 (p. 20) — homogeneous systems

If $r_i=\lambda\in(0,1)$ for all $i$ and there are no exact overlaps, then $\dim_H\mu=\min\{1,H(p)/\log(1/\lambda)\}$.

Goal: Theorem 1.1 (p. 2)

For every such family and every strictly positive probability vector $p$,

$$\dim_H\mu=\min\Bigl\{1,\ \frac{h_{RW}}{\chi}\Bigr\}.$$

No separation assumption is made; exact overlaps and repeated generators are allowed.

Significance

The result itself. It removes every arithmetic and separation hypothesis from the dimension theory of self-similar measures on the line: the only way dimension can drop below $\min\{1,H(p)/\chi\}$ is through exact overlaps, and then the drop is exactly measured by the map entropy. Without exact overlaps it gives the classical formula (Corollary 6.2, p. 19), and hence the dimension of every self-similar set without exact overlaps (Corollary 6.3), which is the exact-overlaps conjecture for sets. It asserts nothing about absolute continuity.

Formalizing it. Hausdorff dimension and self-similar measures exist only partially in Mathlib, and the proof needs a quantitative entropy calculus for finite laws at multiple scales. A formal proof would certify the general theorem together with the consequences that previously required separate arithmetic hypotheses. The only external input is the Feng–Hu exact-dimensionality theorem.

Difficulty

Hochman's method yields the formula under exponential separation of cylinders, but Baker and Bárány–Käenmäki showed that without exact overlaps cylinders can still come superexponentially close, so no lower bound on the separation is available, and exact overlaps add further collisions. The proof must therefore detect entropy hidden at arbitrarily fine scales with no control on the smallest positive distance. The preprint does this with a finite-law pair estimate independent of minimal separation (Lemma 3.2, p. 9), conditioning on block types to recover the map-entropy rate when addresses collide (Lemma 4.1, p. 13), and disjoint windows of entropy gain whose depths are chosen adaptively (Section 5).

Formalization scope

• A System ι over a nonempty Fintype ι carries ratio, offset, weight with $0<|r_i|<1$, $p_i>0$, $\sum p_i=1$. SelfSimilar S μ is the equation $\mu=\sum_i p_i\,(\varphi_i)_*\mu$ for a probability measure $\mu$ on $\mathbb R$.
• wordAffine composes maps as $\varphi_{i}\circ\varphi_w$ and records (slope, translation); mapMass merges words with equal complete maps; walkEntropy n is base-2 Shannon entropy of $G_n$; entropyRate is the sInf over $n\ge1$ of $H(G_n)/n$; lyapunov is base-2.
• lowerHausdorffDimension μ is an iInf in ℝ≥0∞ of dimH E over measurable $E$ with $\mu(E)>0$; the goal compares it to ENNReal.ofReal (min 1 (h/χ)).
• NoExactOverlaps is injectivity of wordAffine on all words; words of different lengths always differ in slope modulus, so this matches the same-length condition of the source. The homogeneous milestone allows a single map, a degenerate case where both sides are $0$.
• The attractor milestone uses its own coding map codingPoint and word functions, equivalent to the definitions above.

Selected references

• OpenAI, The entropy-rate dimension formula for self-similar measures on the line, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf
• P. P. Varjú, Entropy rates in the dimension theory of self-similar measures, arXiv:2509.22042 (2026). https://arxiv.org/abs/2509.22042v2
• J. E. Hutchinson, Fractals and self-similarity, Indiana Univ. Math. J. 30 (1981). https://doi.org/10.1512/iumj.1981.30.30055
• D.-J. Feng, H. Hu, Dimension theory of iterated function systems, Comm. Pure Appl. Math. (2009). https://doi.org/10.1002/cpa.20276
• M. Hochman, On self-similar sets with overlaps and inverse theorems for entropy, Ann. of Math. 180 (2014). https://doi.org/10.4007/annals.2014.180.2.7
• P. P. Varjú, On the dimension of Bernoulli convolutions for all transcendental parameters, Ann. of Math. 189 (2019). https://doi.org/10.4007/annals.2019.189.3.9
• E. Breuillard, P. P. Varjú, On the dimension of Bernoulli convolutions, Ann. Probab. (2019). https://doi.org/10.1214/18-AOP1324
• A. Rapaport, Proof of the exact overlaps conjecture for systems with algebraic contractions, Ann. Sci. ENS (2022). https://doi.org/10.24033/asens.2518
• A. Rapaport, P. P. Varjú, Self-similar measures associated to a homogeneous system of three maps, Duke Math. J. (2024). https://doi.org/10.1215/00127094-2023-0019
• S. Baker, Iterated function systems with super-exponentially close cylinders, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107548
• B. Bárány, A. Käenmäki, Super-exponential condensation without exact overlaps, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107549
• B. Solomyak, On the random series Σ±λ^n (an Erdős problem), Ann. of Math. (1995). https://doi.org/10.2307/2118556

Motivation

A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds $\nu(B(x,r)) \le K r^\beta$ to the behaviour of projections. This preprint proves explicit, dimension-dependent versions for random exact projections and applies them to a learning question: how many noiseless Gaussian measurements $\langle x_t, s\rangle$ does a learner with $M$ bits of memory need to recover a unit vector $s$ to angular accuracy $\epsilon$?

The answer proved here is that $M = o(d^2)$ bits force $T \ge c\,d\log(1/\epsilon)$ measurements, matching the real-valued randomized Kaczmarz scale, and more generally $T \ge c\,d\log(1/\epsilon)/(1 + M/d^2)$ for every $M$.

Timeline

• 1975. Mattila relates Hausdorff dimension, orthogonal projections and ball-growth measures through inverse-distance energy averaging.
• 1984. Drury's affine-plane change of variables for $k$-plane transforms contains the simplex-volume Jacobian used in projection calculations.
• 2014–2016. Shamir's finite-message framework includes bounded-memory online learning; Steinhardt and Duchi (2015) prove memory-dependent minimax rates for sparse regression; Steinhardt, Valiant and Wager (2016) relate memory, communication and statistical queries; Raz (2016) proves the quadratic-memory versus exponential-sample separation for parity learning.
• 2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample bound for Gaussian regression with small uniform noise, $d^2/4$ bits and Euclidean accuracy $d^{-r}$, using high-moment expansions and successive orthogonalization. Dagan, Kur and Shamir prove quadratic-space bounds for two other linear-prediction tasks.
• 2026. The OpenAI preprint Projection moments, positive cap domination, and Riesz estimates on the sphere (dated September 27, 2026) gives three independent proofs of the $\Omega(d\log(1/\epsilon))$ bound for exact observations and $o(d^2)$ memory. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Let $\sigma$ be uniform probability on $S^{d-1} \subset \mathbb{R}^d$. A finite measure $\nu$ on $\mathbb{R}^d$ satisfies an all-ball mass bound with constants $K, \beta$ if $\nu(B(x,r)) \le K r^\beta$ for every ball. For an orthonormal $k$-frame $P$, $P_\#\nu$ is the image measure on $\mathbb{R}^k$ and $g(P,\cdot)$ its density. The Riesz functional of $h : S^{d-1} \to [0,1]$ is $V(h) = \sup_{z} \int h(s)\|s-z\|^{-d/2}\,d\sigma(s)$.

In the finite-state regression experiment, the signal $S \sim \sigma$; at each step a row $x_t \sim N(0, I_d)$ arrives with its exact label $\langle x_t, S\rangle$. A learner keeps one of $2^M$ states, may use arbitrary measurable randomized transitions of the current state and pair, stops by a deterministic horizon $T$, and outputs a unit vector from its terminal state, stopping index and fresh randomness. Success means $\arccos\langle \hat S, S\rangle \le \epsilon$.

In Lean (OAI.ProjectionMoments, OAI.NoiselessRegression), learners are FiniteKernelLearner d M T (Markov-kernel transitions on completed observations, states Fin (2^M)), mixed over a seed space Ξ with probability ρ; seededSuccess is uniform-prior success; AllBallMass ν K β, coordinateDensity, frameLaw, capMeasure, rieszPotential encode the geometric objects.

Formalization targets

Goal: OAI.ProjectionMoments.main

A conjunction of the paper's results, including:

• Theorem 2.4 (finite-memory precision bound). There is an absolute $c > 0$ such that for every $M(d) = o(d^2)$, eventually in $d$, uniform-sphere success at least $2/3$ at accuracy $0 < \epsilon \le 1/10$ forces

$$T \ge c\, d \log(1/\epsilon),$$

also under an every-signal guarantee.

• Corollary 2.5, in the weakened form that $M \le A d^2$ gives $T \ge c_A d\log(1/\epsilon)$ (the paper proves $T \ge c\,d\log(1/\epsilon)/(1+M/d^2)$).
• Theorem 3.3 (integrated orthonormal-projection moment). If $\nu$ is finite, supported in $B(z,R)$, with $\nu(B(x,r)) \le K r^\beta$, and $k+q \le d$, $0 < \beta \le d$, $\beta - k - (q-2) \ge 1$, then

$$\Big(\iint g(P,u)^q\,du\,d\vartheta_{d,k}(P)\Big)^{1/q} \le C^d (C\sqrt d)^{k(1-1/q)} K R^{\beta - k(1-1/q)}.$$

• Theorem 3.5, Corollary 3.4 and Proposition 3.7 (normalized and all-radii moments, one-block propagation), Proposition 4.1 (positive domination by countable sums of cap measures), Lemma 5.3 (projection density at deterministic offsets), and the explicit success bounds of Propositions 3.8, 4.4 and 5.4 for arbitrary $M$.
• A bridge showing the kernel learner model agrees with the seeded deterministic learner model.

Significance

The result. The projection moment estimates are general statements about finite measures with ball-growth control and apply beyond learning. In the learning application they give three proofs, with different stopping and accuracy costs, that $o(d^2)$ bits cannot beat the $d\log(1/\epsilon)$ sample scale for exact Gaussian measurements, plus an explicit trade-off for all $M$.

Formalizing it. The results are in an unrefereed preprint; there is no machine-checked proof. The conjunct FixedQuadraticMemory coincides with part of the goal of the companion mission on Memory and precision in noiseless Gaussian regression, so progress here is shared.

Difficulty

Integrated density norms do not determine density values on a matrix-dependent graph, so pointwise statements need an explicitly chosen density version. The high moments of projected densities require controlling collisions of $q$ independent points under projection, which leads to inverse affine heights whose integrability must be extracted from the ball-growth hypothesis at all scales. In the learning application, conditioning on an exact label produces a singular posterior, so arguments that track a posterior density fail.

Formalization scope

• Space is EuclideanSpace ℝ (Fin d); frames are orthonormal families Fin k → E drawn by frameLaw; densities are ℝ≥0∞-valued with explicit measurable versions.
• Parameters are natural-number floors (d/4, d/8, d/16); block counts appear as (T+k-1)/k.
• Learners: FiniteKernelLearner with CompletedRules almost surely in the seed; success probabilities are ℝ≥0∞.

The goal has no trivial reading: each conjunct quantifies over all measures or learners satisfying the stated hypotheses, and the hypotheses are satisfiable.

Needed infrastructure: Stiefel and Haar measures, Gaussian polar decomposition of matrices, Gram–Schmidt Jacobians, spherical caps, Riesz potentials. Contributions proving individual conjuncts (for example Theorem 3.3) are welcome.

Selected references

• OpenAI, Projection moments, positive cap domination, and Riesz estimates on the sphere, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Projection-moments-positive-cap-domination-and-Riesz-estimates-on-the-sphere-September-27-2026/paper.pdf
• P. Mattila, Hausdorff Dimension, Orthogonal Projections and Intersections with Planes, Ann. Acad. Sci. Fenn. Ser. A I Math. 1 (1975). https://doi.org/10.5186/aasfm.1975.0110
• S. W. Drury, Generalizations of Riesz Potentials and $L^p$ Estimates for Certain $k$-Plane Transforms, Illinois J. Math. 28 (1984).
• V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403
• R. Raz, Fast Learning Requires Good Memory, 2016. https://arxiv.org/abs/1602.05161
• J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• O. Shamir, Fundamental Limits of Online and Distributed Algorithms for Statistical Learning and Estimation, NeurIPS 2014.
• Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html

Motivation

Draw $n$ independent fair bits $X$, compute a one-bit summary $f(X)$, and send the bits through independent binary symmetric channels with crossover probability $\varepsilon$, producing $Y$. Which summary tells the receiver the most about $Y$? Kumar and Courtade conjectured that a single coordinate, $f(X)=X_1$, is optimal: $I(f(X);Y)\le 1-h_2(\varepsilon)$ bits for every Boolean $f$, in every dimension and at every noise level (ISIT 2013; IEEE Trans. Inf. Theory 2014). The Courtade–Kumar (most informative Boolean function) conjecture is a basic question about how noise destroys information on the discrete cube, connecting information theory with Boolean Fourier analysis and hypercontractivity.

This mission asks for a formal proof of a sharp contraction theorem for arbitrary randomized binary summaries, whose Boolean case is the Courtade–Kumar conjecture, as stated in an OpenAI preprint dated September 24, 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.

Background

• 1970–1976 — Hypercontractivity on the cube (Bonami, Ann. Inst. Fourier 1970; Gross, Amer. J. Math. 1975; Beckner, Annals 1975); Mrs. Gerber's lemma (Wyner–Ziv, IEEE TIT 1973).
• 2013–2014 — Kumar and Courtade pose the conjecture and prove a coordinatewise sum bound.
• 2016 — High-noise results: Ordentlich, Shayevitz and Weinstein for balanced functions (ISIT 2016); Samorodnitsky for all Boolean functions in a dimension-independent high-noise range (IEEE TIT 2016).
• 2018 — Pichler, Piantanida and Matz prove coordinate optimality when the observation is also reduced to one bit (Ann. Appl. Probab. 2018).
• 2020–2023 — Barnes–Özgür's symmetrized reformulation (ISIT 2020); Li–Médard on fixed-mean optimizers (IEEE TIT 2021); Yu's $\Phi$-stability (PTRF 2023).
• 2025–2026 — Chen, Gohari and Nair's differential (entropy-production) approach; independent preprints announcing proofs by Chen, Gohari, Javanmard, Lin, Mirrokni, Nair and Woodruff (arXiv:2609.24931), Ky and Tran (arXiv:2609.24184), Mahdavifar and Beirami (arXiv:2609.26444), and a bias-retaining finite-noise bound by Kramer and Saglam.
• September 2026 — The OpenAI preprint (Theorems 1.1 and 1.3, Corollary 1.2, pp. 1–4).

Setting

Let $\Omega_n=\{-1,1\}^n$ with uniform measure; information is in nats unless stated. For $r\in[-1,1]$ put

$$L=\log2,\quad H(r)=-\tfrac{1+r}2\log\tfrac{1+r}2-\tfrac{1-r}2\log\tfrac{1-r}2,\quad \psi(r)=L-H(r),$$

with $0\log0=0$; $\psi^{-1}$ is the increasing branch $[0,L]\to[0,1]$. A soft channel is $u:\Omega_n\to[-1,1]$, the conditional mean of an auxiliary sign $U$ given $X$; its information is $I(u)=H(\mathbb Eu)-\mathbb EH(u)=I(U;X)$. For $\rho\in[-1,1]$ let $Y_i=X_iZ_i$ with independent signs $\mathbb EZ_i=\rho$, and let $T_\rho u(y)=\mathbb E[u(X)\mid Y=y]$, so $I(T_\rho u)=I(U;Y)$. For an interior field $g:\Omega_n\to(-1,1)$ with $m=\mathbb Eg$, the production is $D(g)=\mathbb E[\operatorname{atanh}(g)\,Ng]$ with $Ng=\frac12\sum_i(g-g\circ\mathrm{flip}_i)$; the rate $F$ is defined by $F(\psi(r))=r\operatorname{atanh}r$; $S(I)=F(I)-2I$ (zero for $I<0$); $B_m(I)=2I+(1-m^2)S\bigl(L-\frac{H(m)-I}{1-m^2}\bigr)$.

Formalization targets

Milestone: Courtade–Kumar inequality in bits (Corollary 1.2, p. 2)

For $n\ge1$, $0\le\varepsilon\le\frac12$ and every Boolean $f$ on $\{0,1\}^n$,

$$I_2(f(X);Y)\le 1-h_2(\varepsilon),$$

with equality for every coordinate $x\mapsto x_i$ and its complement.

Goal: the soft contraction package (Theorem 1.1, p. 1; Corollary 1.2, p. 2; Theorem 1.3, p. 4)

The goal OAI.SoftChannel204.fullMain is the conjunction of:

1. Theorem 1.1. For all $n$, $u:\Omega_n\to[-1,1]$, $\rho\in[-1,1]$:

$$I(T_\rho u)\le\psi\bigl(|\rho|\,\psi^{-1}(I(u))\bigr),$$

with equality for every soft coordinate $u(x)=a x_i$, $|a|\le1$; and $I(U;Y)=I(T_\rho u)$ for the joint law of $(U,Y)$. 2. Corollary 1.2. For Boolean $f$ with $m=\mathbb Ef$ and $r_m=\psi^{-1}(H(m))$: $I(f(X);Y)\le\psi(|\rho|r_m)\le\psi(|\rho|)$, strictly below $\psi(|\rho|)$ when $0<|m|<1$ and $0<|\rho|$; coordinates and their negations attain $\psi(|\rho|)$; and the bits conversion $\psi(1-2\varepsilon)/L=1-h_2(\varepsilon)$. 3. Theorem 1.3. For every interior $g$: $D(g)\ge\max\{B_m(I(g)),F(I(g))\}\ge F(I(g))$.

Significance

The result itself. It settles the Courtade–Kumar conjecture and strengthens it in two directions: to randomized summaries at fixed initial information, and to a bias-dependent bound that is strictly better for nonconstant biased outputs. Theorem 1.3 is a mean-dependent entropy-production inequality, stronger than the scalar rate needed for Theorem 1.1. Several independent proofs of the Boolean conjecture were announced in the same period; the preprint compares its production profile with that of Chen et al. in Section 8.

Formalizing it. All objects are finite sums over $\{-1,1\}^n$, so the statements are elementary to state in Lean. The proof requires an explicit three-point optimizer for a joining problem, convexity facts about $F$ and $S$ (Lemmas 2.2–2.4, pp. 5–6), dimension induction and integration along the noise semigroup. A formal proof would give a checked solution of a conjecture with several competing announced proofs, some computer-assisted.

Difficulty

The local-to-global method of Chen, Gohari and Nair needs a local inequality to pass from the two halves of the cube to the whole. The natural information-only profile $\Phi_m(I)=F(I)$ fails the corresponding local comparison for some coupled pair laws, so the induction must carry the mean $m$ as well. The preprint uses the maximum of two profiles, $B_m$ and $F$; it must solve the minimization of the joining cost exactly (Section 3), pay the interior pair with a variance-refined one-bit inequality (Lemma 4.1, p. 12), and control the common-output corners by a thinning argument (Theorem 6.1, p. 17). The linear bound $D(g)\ge2I(g)$ from the log-Sobolev inequality does not suffice; the nonlinear surplus above $2I$ is where the difficulty lies.

Formalization scope

• Cube n = Fin n → Bool, averages are finite sums divided by $2^n$, logs are natural; sign maps Bool to $\pm1$.
• psiInv is Function.invFunOn psi (Icc 0 1); since $\psi$ is strictly increasing on $[0,1]$ and $I(u)\in[0,L]$, this is the paper's branch.
• noise ρ u y = ∑ x, kernel ρ y x * u x with kernel the product of $(1\pm\rho)/2$, which is $T_\rho$. Mutual information is the finite sum over the joint table, with terms omitted where the joint probability is $0$.
• F is stated as psiInv s * artanh (psiInv s) and is only used on $[0,L)$; for interior $g$, $|m|<1$ and $0\le I(g)<H(m)\le L$, so reserve and hybrid are evaluated in their source domain.
• All results hold for every $n\ge0$; the attainment statements quantify over i : Fin n. The milestone (separate definition file) uses the crossover form with bits.

Selected references

• OpenAI, Sharp binary-information contraction on the discrete cube, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf
• T. A. Courtade, G. R. Kumar, Which Boolean functions maximize mutual information on noisy inputs?, IEEE Trans. Inf. Theory 60 (2014). https://doi.org/10.1109/TIT.2014.2326877
• G. R. Kumar, T. A. Courtade, Which Boolean functions are most informative?, ISIT 2013. https://doi.org/10.1109/ISIT.2013.6620221
• A. Samorodnitsky, On the entropy of a noisy function, IEEE Trans. Inf. Theory (2016). https://doi.org/10.1109/TIT.2016.2584625
• O. Ordentlich, O. Shayevitz, O. Weinstein, An improved upper bound for the most informative Boolean function conjecture, ISIT 2016. https://doi.org/10.1109/ISIT.2016.7541349
• G. Pichler, P. Piantanida, G. Matz, Dictator functions maximize mutual information, Ann. Appl. Probab. (2018). https://doi.org/10.1214/18-AAP1384
• L. Yu, On the $\Phi$-stability and related conjectures, Probab. Theory Relat. Fields (2023). https://doi.org/10.1007/s00440-023-01209-5
• A. Gohari, C. Nair, Outer bounds for multiuser settings: the auxiliary receiver approach, IEEE Trans. Inf. Theory (2022). https://doi.org/10.1109/TIT.2021.3128136
• Z. Chen, A. Gohari, A. Javanmard, et al., A proof of the most informative Boolean function conjecture, arXiv:2609.24931 (2026). https://arxiv.org/abs/2609.24931
• V. K. Ky, T. Tran, Dictators are most informative, arXiv:2609.24184 (2026). https://arxiv.org/abs/2609.24184
• H. Mahdavifar, A. Beirami, The most informative bit and beyond, arXiv:2609.26444 (2026). https://arxiv.org/abs/2609.26444
• S. G. Bobkov, P. Tetali, Modified logarithmic Sobolev inequalities in discrete settings, J. Theoret. Probab. (2006). https://doi.org/10.1007/s10959-006-0016-3

Motivation: keeping partial sums of vectors small

Given vectors $v_1,\dots,v_N$ in the Euclidean unit ball of $\mathbb R^d$ that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on $d$? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius $d$ suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is $O(\sqrt d)$, the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs $\varepsilon_i\in\{\pm1\}$, chosen once and for all, such that every signed prefix $\sum_{i\le k}\varepsilon_iv_i$ is $O(\sqrt d)$, independently of $N$. Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.

Timeline

• 1913 — Steinitz proves his rearrangement lemma for conditionally convergent vector series (historical account in Ambrus–Heck 2026, Section 2).
• 1954 — Behrend discusses the expected square-root growth in Euclidean space (Canad. J. Math., p. 108).
• 1980 — Grinberg and Sevast'yanov prove that partial sums can be kept within $d$ times the unit ball, for every norm (Funct. Anal. Appl.).
• 1994–2023 — Chobanyan's transference principle relates rearrangements to signed sums (Probability in Banach Spaces 9, 1994), later in a finite positive-forward, negative-reverse form (Chobanyan et al., Bull. TICMI 2023).
• 1998 / 2012 — Banaszczyk's Gaussian-measure balancing theorem (Random Structures Algorithms 1998) and his prefix bound $O(\sqrt d+\sqrt{\log N})$ for signed series and rearrangements (Random Structures Algorithms 2012).
• 2021 — Bansal, Jiang, Meka, Singla and Sinha state the $O(\sqrt d)$ prefix-signing question explicitly (Conjecture 6.3, arXiv:2111.07049).
• 2026 — Ambrus and Heck record the conjecture and its attribution to Bergström (Conjecture 5) and reduce it to a relaxed problem (Mathematika); Dutta, Jha and Jiang give efficient bounds $O(\sqrt d+d^{1/4}\log^{7/4}N)$ (arXiv:2604.13355).
• 2026 — An OpenAI preprint, The Euclidean Steinitz–Bergström theorem (OpenAI Math Release, September 24, 2026), claims the $O(\sqrt d)$ bound for both problems with an absolute constant. It has not been peer reviewed, and its proof is not formally verified.

Setting

Work in Euclidean space $\mathbb R^d$ with norm $\|\cdot\|_2$, and let $v_1,\dots,v_N$ satisfy $\|v_i\|_2\le1$; repetitions and zero vectors are allowed. A prefix sum is $\sum_{i=1}^k$ for $0\le k\le N$ (the empty sum is $0$). For a zero-sum family, the Steinitz quantity

$$\beta(v_1,\dots,v_N)=\min_{\pi\in\mathfrak S_N}\ \max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2$$

is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant $S_2(d)$ is its supremum over all such families.

Formalization targets

Goal: prescribed-order signing and Euclidean Steinitz with one absolute constant (Theorems 1.1 and 1.2)

There is an absolute constant $C$ such that for all $d,N\ge1$ and all $v_1,\dots,v_N\in\mathbb R^d$ with $\|v_i\|_2\le1$:

1. (Theorem 1.1) there are signs $\varepsilon_i\in\{-1,1\}$ with

$$\max_{0\le k\le N}\Bigl\|\sum_{i=1}^k\varepsilon_iv_i\Bigr\|_2\le C\sqrt d ;$$

2. (Theorem 1.2) if moreover $\sum_iv_i=0$, some permutation $\pi$ satisfies

$$\max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2\le C\sqrt d .$$

The constant is not fixed. The simplex example in the source shows $S_2(d)\ge\tfrac12\sqrt d$, so the order is optimal. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: $S_2(d)=\Theta(\sqrt d)$. Theorem 1.1 settles the $\ell_2$ prefix-discrepancy question of Bansal et al., removing the $\sqrt{\log N}$ term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional $\ell_p$ Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.

Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.

Difficulty

Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all $N$ prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a $\sqrt{\log N}$ factor, because the probability that a random walk stays in a ball of radius $C\sqrt d$ for $N$ steps decays with $N$. The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin d), indexed by Fin N, with $d,N\ge1$ and $\|v_i\|\le1$.
• Prefixes are sums over $\{i : i < k\}$ for every natural $k\le N$, so the empty prefix and the full sum are included.
• SignedPrefixBound C asks for signs $\varepsilon_i\in\{-1,1\}$ (as reals) with every signed prefix at most $C\sqrt d$. OrderingPrefixBound C asks, for zero-sum families, for a permutation $\pi$ with every reordered prefix at most $C\sqrt d$. The goal is $\exists C,\ \mathrm{SignedPrefixBound}\,C\wedge\mathrm{OrderingPrefixBound}\,C$; the same constant serves both, as stated in the source.
• The quantifier order is the source's: $C$ is chosen before $d$, $N$ and the vectors.
• Needed infrastructure: Gaussian measures of symmetric convex bodies, Steiner symmetrization, Dirichlet energies of densities, Ornstein–Uhlenbeck/Brownian survival estimates, and the Chobanyan transference. Contributions proving the transference step (Theorem 1.1 ⇒ Theorem 1.2) or the lower-bound example are welcome.

Selected references

• V. S. Grinberg and S. V. Sevast'yanov, Value of the Steinitz constant, Funct. Anal. Appl. (1980).
• F. A. Behrend, The Steinitz–Gross theorem on sums of vectors, Canad. J. Math. (1954).
• S. Chobanyan, Convergence a.s. of rearranged random series in Banach space and associated inequalities, Probability in Banach Spaces 9 (1994).
• W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures Algorithms (1998).
• W. Banaszczyk, On series of signed vectors and their rearrangements, Random Structures Algorithms (2012).
• N. Bansal, H. Jiang, R. Meka, S. Singla and M. Sinha, Prefix discrepancy, smoothed analysis, and combinatorial vector balancing, 2021. https://arxiv.org/abs/2111.07049
• G. Ambrus and R. Heck, A note on the Steinitz Lemma, Mathematika (2026). https://doi.org/10.1112/mtk.70085
• K. Dutta, A. V. Jha and H. Jiang, Near-optimal constructive bounds for $\ell_2$ prefix discrepancy and Steinitz problems via affine spectral independence, 2026. https://arxiv.org/abs/2604.13355
• OpenAI, The Euclidean Steinitz–Bergström theorem, OpenAI Math Release preprint, September 24, 2026 (Theorems 1.1 and 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026.pdf

Motivation: the triangular Hilbert transform

The triangular Hilbert transform is a bilinear singular integral on the plane that couples translations in two different coordinate directions:

$$B(F,G)(x,y)=\mathrm{p.v.}\!\int_{\mathbb R}F(x+t,y)\,G(x,y+t)\,\frac{dt}{t}.$$

Paired with a third function, it becomes a trilinear form whose three inputs depend on the three pairs of variables of $(a,b,c)$. This "triangular" or entangled structure defeats the time–frequency methods that handle the one-dimensional bilinear Hilbert transform. Boundedness of this operator is a model problem for multilinear singular integrals with simplex structure, and is closely tied to norm convergence and variation of ergodic averages for two commuting transformations. Thiele listed the symmetric case ($L^3\times L^3\times L^3$) as Problem 13 in the 2017 collection Some problems in harmonic analysis.

Timeline

• 2010 — Demeter and Thiele study the two-dimensional bilinear Hilbert transform and highlight the flat triangular operator (Amer. J. Math.).
• 2012 — Kovač proves boundedness of the twisted paraproduct, a bipartite relative of the triangular form, by energy telescoping (Rev. Mat. Iberoam.).
• 2015 — Kovač, Thiele and Zorin-Kranich prove bounds for a Walsh (dyadic) model with one structurally restricted input (Forum Math. Sigma).
• 2016–2017 — Tao proves sublogarithmic cancellation for multilinear Hilbert transforms (Collect. Math.); Zorin-Kranich extends it to simplex Hilbert transforms (Math. Res. Lett.); Thiele's problem appears in Grafakos et al. (arXiv:1701.06637).
• 2019 — Durcik, Kovač, Škreb and Thiele obtain square-root cancellation across finitely many smooth scales (Ergodic Theory Dynam. Systems); Durcik, Kovač and Thiele prove power-type cancellation with hard truncations, still growing like $\sqrt{\log(R/\varepsilon)}$ at the symmetric point (J. Anal. Math.).
• 2021 — Durcik and Roos bound averages over directions (Proc. AMS); Christ, Durcik and Roos treat the curved variant along $(t,t^2)$ (Adv. Math.).
• 2026 — An OpenAI preprint, The maximal triangular Hilbert transform at the symmetric point (OpenAI Math Release, September 24, 2026), claims the scale-free $L^3\times L^3\to L^{3/2}$ bound for the maximal truncated operator. It has not been peer reviewed, and its proof is not formally verified.

Setting

For complex functions $F,G$ on $\mathbb R^2$ and $0<\varepsilon<R<\infty$, the hard truncation is

$$B_{\varepsilon,R}(F,G)(x,y)=\int_{\varepsilon<|t|<R}F(x+t,y)\,G(x,y+t)\,\frac{dt}{t},$$

and the maximal truncation is

$$B_*(F,G)(x,y)=\sup_{0<\varepsilon<R<\infty}\bigl|B_{\varepsilon,R}(F,G)(x,y)\bigr| .$$

For $F,G\in L^3(\mathbb R^2)$ the finite truncations converge absolutely outside a common null set, and $B_*$ is measurable (Lemma 7.1 of the source).

Formalization targets

Goal: the maximal triangular Hilbert transform is bounded at the symmetric point (Theorem 1.1)

There is an absolute constant $C$ such that, for all complex $F,G\in L^3(\mathbb R^2)$,

$$\|B_*(F,G)\|_{L^{3/2}(\mathbb R^2)}\le C\,\|F\|_{L^3(\mathbb R^2)}\|G\|_{L^3(\mathbb R^2)} .$$

The Lean goal also includes the measure-theoretic preliminaries of Lemma 7.1: almost every point is a point where all finite truncations converge absolutely, and $B_*$ is almost-everywhere measurable. The goal statement is published on the platform with status Open.

Significance

The result itself. A uniform bound for the maximal operator controls a truncation chosen independently at each point, which is stronger than a uniform bound on each $B_{\varepsilon,R}$. It yields existence of the joint principal value $B(F,G)$ almost everywhere and in $L^{3/2}$ (Theorem 7.2). By duality and a determinant-one change of variables, it gives endpoint-uniform bounds for the symmetric trilinear triangular form $\iiint G_0(a,b)G_1(b,c)G_2(c,a)\,\frac{da\,db\,dc}{a+b+c}$, which resolves Thiele's Problem 13 positively. Earlier bounds all grew with the number of scales.

Formalizing it. The estimate is a clean statement in Mathlib's $L^p$ and lower-integral language. Its proof combines matrix trace inequalities, Gaussian heat-flow energies and discretization limits, all of which would have to be built. The finite-dimensional matrix inequalities (Sections 2–3 of the source) are self-contained and reusable for other entangled multilinear forms.

Difficulty

Time–frequency analysis, which handles the one-dimensional bilinear Hilbert transform, does not adapt to the triangular form because its three inputs are entangled: each depends on a different pair of variables, so no single frequency-localization serves all three. Energy and telescoping methods (Kovač; Durcik) work for bipartite forms, but the triangular cycle is the documented obstruction. Previous cancellation estimates lose a factor depending on the number of scales $\log(R/\varepsilon)$. The maximal version adds a further difficulty: the truncation endpoints vary from point to point, so the energy argument must tolerate entries that switch on and off at independently chosen scales, without losses depending on the number of scales or on matrix dimensions.

Formalization scope

• Functions are ℝ × ℝ → ℂ with Lebesgue measure; hypotheses are MemLp F 3 and MemLp G 3 (which include a.e. strong measurability).
• truncation F G E z is the Bochner integral of $F(x+t,y)G(x,y+t)/t$ over $\{\varepsilon<|t|<R\}$, with endpoints packaged as Endpoints ($0<\varepsilon<R$).
• GoodPoint requires integrability on the annuli $1/(n+2)<|t|<n+2$ for all $n$, hence on every finite annulus. maximal is the ℝ≥0∞-valued supremum over all endpoint pairs at good points, and $0$ elsewhere. The goal asserts that almost every point is good, so this junk value cannot help.
• The norm is $\bigl(\int^- B_*^{3/2}\bigr)^{2/3}$ in ℝ≥0∞, compared with eLpNorm F 3 * eLpNorm G 3. The constant is an existential ℝ≥0, so it is finite and independent of $F,G$.
• Needed infrastructure: discretization of $L^3$ functions, finite-dimensional trace inequalities for $\operatorname{tr}((R^*R)^{3/2})$, Gaussian heat-flow monotonicity, one-dimensional Hardy–Littlewood maximal bounds, and limits of smooth truncations. Contributions on the matrix inequalities or the jump-control lemma are welcome.

Selected references

• C. Demeter and C. Thiele, On the two-dimensional bilinear Hilbert transform, Amer. J. Math. (2010). https://doi.org/10.1353/ajm.0.0101
• V. Kovač, Boundedness of the twisted paraproduct, Rev. Mat. Iberoam. https://doi.org/10.4171/RMI/707
• V. Kovač, C. Thiele and P. Zorin-Kranich, Dyadic triangular Hilbert transform of two general functions and one not too general function, Forum Math. Sigma (2015). https://doi.org/10.1017/fms.2015.25
• T. Tao, Cancellation for the multilinear Hilbert transform, Collect. Math. (2016). https://arxiv.org/abs/1505.06479v3
• P. Zorin-Kranich, Cancellation for the simplex Hilbert transform, Math. Res. Lett. (2017). https://doi.org/10.4310/MRL.2017.v24.n2.a16
• L. Grafakos, D. Oliveira e Silva, M. Pramanik, A. Seeger and B. Stovall, Some problems in harmonic analysis (2017), Section 9, Problem 13. https://arxiv.org/abs/1701.06637v1
• P. Durcik, V. Kovač, K. A. Škreb and C. Thiele, Norm-variation of ergodic averages with respect to two commuting transformations, Ergodic Theory Dynam. Systems (2019). https://doi.org/10.1017/etds.2017.48
• P. Durcik, V. Kovač and C. Thiele, Power-type cancellation for the simplex Hilbert transform, J. Anal. Math. (2019). https://doi.org/10.1007/s11854-019-0052-4
• OpenAI, The maximal triangular Hilbert transform at the symmetric point, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2; Lemma 7.1, p. 24). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026/paper.pdf

Motivation

Finite games in strategic form are the basic model of strategic interaction in economics, engineering and computer science. Potential games (Monderer and Shapley, 1996, DOI 10.1006/game.1996.0044) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics converge to one.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) decompose every finite game canonically into a potential, a harmonic and a nonstrategic component, by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games are the complement of potential games, and their equilibria behave in the opposite way: they generically have no pure Nash equilibrium. This mission formalizes the paper's positive result on the harmonic side. In every harmonic game, whatever the number of players and strategies, the profile in which every player randomizes uniformly over its strategies is a mixed Nash equilibrium. Rock–paper–scissors and matching pennies are the familiar two-player instances.

Setting

A finite game has a finite set of players $\mathcal M$ and, for each player $m$, a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$. We write $p^{-m}$ for the strategies of the players other than $m$, $E^{-m} = \prod_{k\ne m}E^k$, and $(q^m, p^{-m})$ for $p$ with player $m$'s strategy replaced by $q^m$. A game is identified with its utilities $u = (u^m)_m$, $u^m : E \to \mathbb R$, which form an element of $C_0^M$, where $C_0 = \{f : E\to\mathbb R\}$ carries $\langle\varphi_1,\varphi_2\rangle_0 = \sum_p\varphi_1(p)\varphi_2(p)$.

Two profiles are $m$-comparable if they are distinct and differ only in player $m$'s strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function $X$ on ordered pairs of profiles with $X(p,q) = -X(q,p)$ on edges and $X = 0$ off edges. The space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\in A}X(p,q)Y(p,q)$. The combinatorial gradient is $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$, with $W$ the edge indicator, and $\delta_0^*$ is its adjoint. Restricting to $m$-comparable pairs gives $D_m : C_0\to C_1$, and $Du = \sum_m D_m u^m$ is the flow of payoff differences of $u$. With $\Pi_m = D_m^\dagger D_m$ (Moore–Penrose pseudoinverse) and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$, Definition 4.2 of the paper sets

$$\mathcal H = \{u \mid u = \Pi u,\ Du \in \ker\delta_0^*\},\qquad \mathcal N = \ker D .$$

A game is a harmonic game if $u\in\mathcal H\oplus\mathcal N$, and a normalized harmonic game if $u\in\mathcal H$.

A mixed strategy of player $m$ is a probability vector $x^m\in\Delta E^m$, and a mixed strategy profile is $x = \{x^m\}_m\in\prod_m\Delta E^m$. The mixed extension is $u^m(x) = \sum_{p\in E}u^m(p)\prod_k x^k(p^k)$ (34). The payoff of the pure strategy $q^m$ against $x^{-m}$ is $u^m(q^m,x^{-m}) = \sum_{p^{-m}}u^m(q^m,p^{-m})\prod_{k\ne m}x^k(p^k)$ (35). A mixed Nash equilibrium (Definition 5.1.1) is a mixed profile with $u^m(x^m,x^{-m})\ge u^m(p^m,x^{-m})$ for every $m$ and $p^m\in E^m$. A probability distribution $x\in\Delta E$ on profiles is a correlated equilibrium (Definition 5.1.2) if $\sum_{p^{-m}}(u^m(p^m,p^{-m})-u^m(q^m,p^{-m}))\,x(p^m,p^{-m})\ge 0$ for all $m$ and $p^m,q^m$. The uniformly mixed strategy profile (Definition 5.2) has $x^m(q^m) = 1/h_m$ for every $m$ and $q^m$.

Formalization targets

Goal: Theorem 5.4

For every harmonic game $u\in\mathcal H\oplus\mathcal N$, the uniformly mixed strategy profile $x$ is a mixed Nash equilibrium:

$$u^m(x^m,x^{-m}) \;\ge\; u^m(p^m,x^{-m})\qquad\text{for all } m\in\mathcal M,\ p^m\in E^m .$$

Milestones

1. Lemma A.1: for every edge flow $\hat X$ and every set of profiles $\hat S$, $\sum_{p\in\hat S}(\delta_0^*\hat X)(p) = -\sum_{p\in\hat S}\sum_{q\in\hat S^c}\hat X(p,q)$.
2. Lemma 5.2: in a harmonic game, $\sum_{p^{-m}\in E^{-m}}\big(u^m(r^m,p^{-m}) - u^m(q^m,p^{-m})\big) = 0$ for all $m$ and $q^m, r^m$.
3. Proposition 5.2: in a normalized harmonic game, a distribution $x\in\Delta E$ is a correlated equilibrium iff all the inequalities of Definition 5.1.2 hold with equality (36), iff $\sum_{p^{-m}}u^m(q^m,p^{-m})\,x(p^m,p^{-m}) = 0$ for all $m,p^m,q^m$ (37).
4. Remark after Proposition 5.2: the equivalence of correlated equilibrium with (36) holds for all harmonic games.
5. Corollary 5.2: in a harmonic game, a mixed profile is a mixed Nash equilibrium iff $u^m(x^m,x^{-m}) = u^m(p^m,x^{-m})$ for all $m$ and $p^m$ (42).

Significance

Theorem 5.4 is the counterpart, for harmonic games, of the existence of pure equilibria in potential games. It exhibits an explicit equilibrium that does not depend on the payoffs at all, only on the strategy counts $h_m$. Corollary 5.2, a milestone here, adds that at any mixed equilibrium of a harmonic game every player is indifferent among all its pure strategies, including those outside the support. That is much stronger than the usual support condition. Proposition 5.2 shows that the correlated equilibria of a normalized harmonic game are the points of the probability simplex in a linear subspace determined by the utilities. The paper uses that description in its later analysis of two-player harmonic games.

The results are proved in the paper; none of them is machine-checked. The formalization connects the paper's operator layer (flows on the game graph, the gradient and its adjoint with the $\tfrac12$-weighted inner product, pseudoinverses) with standard equilibrium notions on finite games. It reuses published definitions of lotteries, the mixed extension and correlated equilibria.

Difficulty

The equilibrium statement follows quickly once Lemma 5.2 is available. The difficulty lies in translating the harmonic condition, a statement about the adjoint of an operator on edge flows, into an identity about payoffs. That needs the explicit form of $\delta_0^*$, which depends on the $\tfrac12$ in the inner product of $C_1$. It also needs the fact that $D$ kills the nonstrategic component, and a computation of the flow of $Du$ across the boundary of the set of profiles in which player $m$ plays $r^m$. Corollary 5.2 needs the passage from mixed profiles to product distributions on profiles and a careful accounting of sums over $p^{-m}$ against sums over full profiles.

The first idea, to use the normalization $\sum_{q^m}u^m(q^m,p^{-m}) = 0$, is not available. The goal concerns all harmonic games, not only normalized ones, and normalization alone does not give indifference against uniform opponents: the harmonic condition is essential.

Formalization scope

Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper ($E^m = \{1,\dots,h_m\}$). The hypothesis [∀ m, Nonempty (E m)] is stated explicitly on the game theorems, because the uniform profile $1/h_m$ is a probability vector only if $h_m\ge1$. A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted sum inner product of p. 14. $C_1$ is the subspace of edge flows with the inner product $\tfrac12\sum$ of (7). $\delta_0^*$ is Mathlib's adjoint, and the pseudoinverse is defined directly. $\mathcal H$ and $\mathcal N$ are defined by (28), and harmonic games are the submodule H ⊔ N. Lotteries, mixed profiles and the mixed extension (34) come from the published agt_games definitions; correlated equilibrium is the published HartSchmeidler.Finite.IsCorrelatedEq. The pure-deviation payoff (35), mixed Nash equilibrium with pure deviations (Definition 5.1.1, as printed), and the uniform profile are defined in the mission. Sums over $p^{-m}$ are written as sums over the profiles with player $m$'s strategy fixed, so each $p^{-m}$ is counted once.

The goal concerns mixed Nash equilibria. Stating it for the uniform product distribution as a correlated equilibrium, or for normalized games only, would be a weaker statement and is not the target. No hypothesis is added beyond the nonemptiness of the strategy sets.

Contributions welcome: proofs of the milestones, and general lemmas on adjoints of graph gradients and on product distributions that are reusable beyond this mission.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3), 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14, 1996. https://doi.org/10.1006/game.1996.0044
• S. Hart, D. Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14(1), 1989. https://doi.org/10.1287/moor.14.1.18