Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Character sums express phase constraints on complex Hadamard matrices. In dimension six these constraints also bear on how many mutually unbiased bases can coexist. The pinned manuscript supplies the research context.
A complex Hadamard matrix has unit-modulus entries and conjugate-transpose product 6I. Equivalence permits row and column permutations and unit phases. Tao's cubic matrix supplies the exceptional class.
The selected goal is OAI.MUB6.fourier_and_family_bound. Its central assertion is
The theorem states a conjunction of two claims about 6x6 complex matrices and mutually unbiased bases in C^6. First, for every complex Hadamard matrix H of order 6 (all entries of modulus 1 and HH = 6I, where H is the conjugate transpose) that is not equivalent to the specific matrix tao, every permutation π of the six coordinates gives g(H, alpha∘π) = 0. Here the character of a column x at an integer exponent vector a is the product over i of x_i^{a_i}, g(H,a) is (1/6) times the sum over the six columns k of H of the character of column k at a, and alpha is the exponent vector (1,1,1,-1,-1,-1), so alpha∘π is alpha with its entries permuted. Equivalence of H and K means K_{ij} = u_i H_{r(i),c(j)} v_j for some row and column permutations r, c and unit-modulus complex phase vectors u and v. The matrix tao has entries ω^{e_{ij}}, where ω = exp(2πi/3) and e is a fixed 6x6 exponent matrix with zero first row and column and a five-cycle pattern of exponents 0, 1, 2 in the remaining 5x5 block. Second, for every natural number n, if there exist n orthonormal bases of C^6 that are pairwise mutually unbiased, meaning |<b_i, b'_j>|^2 = 1/6 for all vectors of two distinct bases, then n ≤ 5. This is stated as an admitted theorem, not a verified proof.
The goal is the conjunction of Fourier vanishing outside the specified equivalence class and the bound on attainable families. The cube-fiber statement is an additional published supporting target with its own hypotheses. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Orthogonality immediately kills certain degree-two characters, but the target concerns a balanced degree-six character and a separate global bound on families of bases.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Signed tensor components separate different sources of permutation symmetry. The source uses their diagram entropies to budget high moments of the Thorp sweep. The source is OpenAI's September 2026 manuscript.
A signed occurrence is an injective equivariant map from a tensor product of three Specht modules into the target module, with the second factor transposed. The weighted moment is the target dimension times the trace of a power of the sweep’s positive square.
There is a constant η₀>0 such that for every η with 0<η<η₀ there is a κ₀ with 0<κ₀<η/256 such that for every κ with 0<κ<κ₀ there is a positive integer power r, depending only on η and κ, with the following property for every d≥1. Let λ be a partition of 2^d (a Young diagram with 2^d cells), and let u+v+l=2^d with partitions α of u, β of v and γ of l, such that the signed occurrence condition holds: there is an injective complex-linear map from the tensor product of the Specht modules S^α ⊗ S^(β′) ⊗ S^γ, where β′ is the transpose of β, into S^λ that commutes with the action of S_u×S_v×S_l, embedded in S_(2^d) as block permutations on the consecutive blocks of sizes u, v and l. Here Specht modules are the cyclic submodules of the regular representation of the symmetric group generated by the polytabloid built from the row and column subgroups of a fixed tableau. Identify {0,…,2^d−1} with binary strings of length d, and for each coordinate i let the layer operator be the average of S^λ over the subgroup of permutations preserving every binary coordinate except the i-th. Let the sweep operator be the product of these d layer operators in reverse coordinate order, and let the sweep square be TT with T the sweep operator. Define the weighted moment as dim S^λ times the real part of tr((TT)^r). Then the logarithm of this moment, taken as −∞ when the moment is zero, is at most coefficient(η,d)·H(α,β) + remainderBudget(κ,d,l). Here coefficient(a,d)=a(1−1/(2√d)), the signed entropy H(α,β) is the sum, over all row lengths a of α and of β, of a·log((u+v)/a), and the remainder budget is 0 if l=0 and otherwise max(0, coefficient(κ,d)·l·log(2^d) − l·log(2^d/l)).
The goal is OAI.SignedSweeps.signed_occurrence_moment_bound. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The target makes the moment power depend only on two small budget parameters, uniformly over cube dimension and every signed occurrence. Supporting targets include the type-angle estimate and a shared mixing bundle. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Ignoring the signed occurrence hypothesis loses the representation-theoretic connection between the component diagrams and the target. The remainder diagram must be charged separately, including its empty case.
The quantifier order is , then each small , then , then each small , then one positive integer . Zero moments have logarithm minus infinity in EReal. Independent source groups stay separate references.
The shared definitions are supplied by SignedSweepMoment, SpinAngle, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Escape to infinity can be arbitrarily slow for a general stochastic process. The source asks whether independent uniformly elliptic lattice environments force a positive deterministic speed whenever a direction is transient. The source is OpenAI's September 2026 manuscript.
Uniform ellipticity provides one positive lower bound for all step probabilities, almost surely at every site. Directional transience means the position projected onto a fixed unit vector tends to positive infinity almost surely under the law averaging environment and walk.
The theorem (admitted, not proved here) states that, for every dimension d ≥ 2 and every Borel probability measure ν on the set of transition rows (a row is a probability vector p over the 2d nearest-neighbour directions ±e_i of ℤ^d, with entries nonnegative and summing to 1), the following holds. Suppose ν is uniformly elliptic, meaning there is κ > 0 with p(e) ≥ κ for every direction e, for ν-almost every row p. Let ℓ be a unit vector in ℝ^d (ℓ·ℓ = 1), and suppose the walk is directionally transient in direction ℓ. Here the environment assigns to each site of ℤ^d an independent ν-distributed row, the walk starts at the origin and at each step moves from its current site x in direction e with probability given by the row at x, and the annealed law averages over the environment and the walk. Directional transience means that, almost surely under this annealed law, the inner product of the walk position X_n with ℓ tends to +∞ as n → ∞. The conclusion is that there exists a vector v ∈ ℝ^d with v·ℓ > 0 such that the walk has asymptotic velocity v, that is, X_n/n → v as n → ∞ almost surely under the annealed law. In other words, directional transience of an i.i.d. uniformly elliptic random walk in random environment in dimension at least two implies ballisticity with a nonzero velocity having positive component along ℓ.
The goal is OAI.DirectionalTransience.directional_transience_implies_ballisticity. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The chosen central target converts almost-sure transience to a velocity statement in every dimension at least two. The separate dimension-at-least-three statement starts from positive probability and identifies the transient hemisphere. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Transience controls eventual direction but not the time spent in traps. A law of large numbers with positive projected velocity needs quantitative control of these delays.
The main statement assumes , a unit direction, and an independent identically distributed uniformly elliptic environment. The supporting hemisphere target assumes and a nonzero direction. Their original definition groups stay separate.
The shared definitions are supplied by DirectionalBallisticity, VelocityHemisphere. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Configuration linear programs relax bin packing by allowing fractional combinations of feasible bins. The mission asks whether the integral optimum can stay within any universal additive constant of this relaxation. The source manuscript presents the surrounding research claim.
A bin-packing instance lists rational item sizes in (0,1]. Feasible bins have total load at most one. The formal development specifies both an individual-item configuration LP and a type-based configuration LP, plus binary encodings of instances, assignments and reductions.
For every natural c, construct I and B with 5B items of sizes strictly between 1/6 and 1 such that
Also prove NP-hardness of every fixed additive packing gap, existence of a polynomial-time absolute-additive algorithm iff P=NP, and the specified exact algorithm consequences under P=NP.
The selected formal target is OAI.BinPackingGap.main_results.
The goal combines unbounded relaxation gaps with a complexity characterization of constant-additive approximation. Item sizes above 1/6 force every bin to hold at most five items. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A large LP gap does not by itself supply NP-hardness. The reduction must have the stated completeness and soundness while preserving the explicit encoding and item-size constraints.
Reductions are finite-alphabet polynomial-time machines from every encoded NP language. The P=NP consequence includes exact optimal bin count, the canonical empty-instance answer and rejection of malformed or invalid input. All clauses of main_results are retained.
adc7f1241b42. Goal source.Mean-payoff games ask which starting positions allow a player to guarantee a nonnegative long-run average reward. Binary-encoded weights make the bit cost of solving the complete winning set a central part of the question. The source manuscript presents the surrounding research claim.
A game is a finite nonempty directed multigraph with integer edge weights, an owner for each vertex and an outgoing edge everywhere. Winning means that a history-dependent maximizer strategy guarantees liminf average payoff at least zero against every opponent strategy.
Construct one randomized three-tape machine and C>0 such that every encoded game of length L has a time bound
all T-bit random tapes halt by T, and at least 7/8 of them output the exact winning-set indicator, with all other output cells blank.
The selected formal target is OAI.randomized_quasipolynomial_mean_payoff.
The target makes the input encoding, computation model, success fraction and complete output explicit. It is an existence theorem for a uniform machine, not a separate solver for each game. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
The running time must hold on every random tape, while correctness holds on the specified fraction. Signed weights and the full binary input length cannot be replaced by unary magnitude bounds.
The published definitions specify games, strategies, plays, liminf payoffs, serialization and tape transitions. The independent finite Truffet elimination counterexample is retained as contextual reference; it is not a prerequisite or an asserted proof of the randomized algorithm. The manuscript’s certification/always-correct consequence is not an additional attached goal.
adc7f1241b42. Goal source.A slope-field perturbation of a two-cylinder cover trades a reduction in projected area against the extra overlap needed to maintain coverage. The slope-field manuscript studies when the net cost becomes strictly smaller. The companion radial-sweep manuscript establishes finite triangular approximation with arbitrary tagged equal subdivisions. Both manuscripts map to the same published Lean goal, so this draft covers their shared target. The source manuscript presents the surrounding research claim.
A cylinder is a measurable finite-area planar base plus a line in its perpendicular unit direction. Ruled sets vary the segment direction over compact planar labels. Radial sweeps use p₀+ρ(a+tb)+s(e+w(t)), with 0≤ρ≤R(t), |s|≤L, and w′(t)=λ(t)(a+tb).
Prove the seven-part fourPaperMain conjunction: the explicit angular-area construction; C¹ hyperbolic approximation; C¹ square-zero-derivative approximation; regular-tetrahedron counterexamples with parallelogram bases and with bounded open bases; aligned radial triangular approximation; and actual-sweep projection bounds. In particular, the tetrahedron clauses require
The selected formal target is OAI.CylinderCovering.fourPaperMain.
The selected published goal is a joint endpoint shared by four related manuscripts, and therefore includes more than the slope-field application alone. Its finite covers retain both cost inequalities. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
A local area decrease cannot guarantee a global cover. All regularity, exact coverage and error bounds in the separate conjuncts must hold in their stated regimes.
Hyperbolic and nilpotent clauses use their C¹ definitions; radial data require a nonempty parameter interval, positive segment half-length, continuous nonnegative cap and alignment derivative. All tagged equal subdivisions are covered. The radial clause requires triangular-base area to converge to weightedArea(D), while actual sweep projections have eventual cost at most weightedArea(D)+ε and the corresponding limsup bound. The separate RuledApproximation.fullMain is also retained as a related reference but is not mislabeled as one of these seven conjuncts.
adc7f1241b42. Goal source.Given a source probability measure and a target on , Brenier's theorem (Brenier 1991) says that when is absolutely continuous there is a unique map pushing to that minimizes the quadratic cost , and that it is the gradient of a convex function. Fixing , the assignment embeds the space of probability measures into ; this linearization of optimal transport is used in statistics, data analysis and machine learning to compare measures by comparing their maps. Its usefulness depends on quantitative stability: how far apart can and be when and are close in Wasserstein distance? For general targets the map cannot be Lipschitz in the target, and the question is which Hölder exponent holds uniformly.
This mission asks for a machine-checked proof that, for a uniform source on a convex body, the sharp uniform exponent is exactly , as claimed in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal below is open.
Fix , a compact convex with nonempty interior, and the uniform source . Fix a nonempty compact and let be the Borel probability measures with . A coupling of is a probability measure on with marginals , and
For , is the Brenier map: a measurable with whose graph coupling is the unique optimal coupling of and . Distances between maps are measured in : .
For every , with and every ,
and the supremum stays infinite when both targets have exactly three atoms. In Lean (one_third_exponent_is_sharp): for every and there are distinct three-atom probability measures on the cube with unique optimal maps and .
For every , as above there is a finite constant such that for all the Brenier maps exist, are unique, and
The targets may be atomic, singular or absolutely continuous; the constant does not depend on them. In Lean this is one_third_stability. Together the two statements determine the sharp exponent in this uniform class, which is the second sentence of Theorem 1.1.
The result itself. The upper bound improves every earlier target-uniform exponent (, , , in or ) to in , with a constant independent of atom counts, atom masses, separations and density bounds. The lower bound disproves Letrouit's conjectured exponent with only three atoms on a cube. The pair gives the exact uniform stability exponent of the linearized optimal-transport embedding for uniform convex sources.
Formalizing it. Mathlib has measures, couplings and Lebesgue integration but no optimal-transport theory. A formal development would supply Wasserstein distance, existence and uniqueness of Brenier maps for semi-discrete and general targets, and Lipschitz convex potentials, all reusable. The sharpness statement is the more elementary one and is a natural first milestone.
The standard route bounds the difference of convex potentials and then converts it to a gradient bound by an interpolation inequality; previous potential estimates lose a power, giving exponents below . The preprint's key step is a linear bound on the distance of potentials, obtained by moving the sites of finite targets along an optimal coupling with fixed masses and controlling the intercept velocity through a uniform moment inequality for the cells of a maximum of affine functions (Lemma 4.1, p. 9; Proposition 5.1, p. 12). The constant must stay uniform as cell masses or faces degenerate, which rules out any argument relying on a spectral gap of the cell graph Laplacian. The final passage from finite to arbitrary Borel targets needs stability of optimal maps under approximation (Proposition 6.3, p. 16).
EuclideanSpace ℝ (Fin d) with Borel measures. uniformMeasure K is ; with compact convex with nonempty interior its volume is positive and finite.IsSupported μ Y means . Couplings are probability measures with the two marginals; costs are lower integrals in ℝ≥0∞; is the square root of the real part of the infimal cost, finite here because supports are bounded.IsUniqueQuadraticOptimalMap ρ μ T asserts that is measurable, pushes to , is cost-optimal among all couplings, and that every coupling of no larger cost equals the graph coupling. The goal must therefore also produce the Brenier maps; they are not assumed.The Boltzmann equation describes a dilute gas through a density of particles at position with velocity , evolving by free transport and binary collisions. For hard spheres, the collision rate is proportional to the normal relative speed. In 1989 DiPerna and Lions constructed global renormalized solutions for all initial data with finite mass, energy and entropy, and weak stability holds at the same level. Existence and stability do not give uniqueness, though: the physical bounds do not even make the quadratic collision term locally integrable, and the uniqueness of general renormalized solutions is a basic question in kinetic theory (Silvestre 2022, §2). Uniqueness is known only under much stronger assumptions, such as Maxwellian upper bounds or closeness to equilibrium.
Phase space is , with . For incoming velocities and a collision normal , put , , . The hard-sphere collision operator is
with ordinary surface measure on ; the two terms are the gain and the loss. The Cauchy problem is , . An initial datum has finite entropy if it is nonnegative and .
A solution is admissible (Definition 2.1 of the source) if, with :
There is a nonnegative finite-entropy datum with bounded velocity support, two admissible global solutions with initial datum , and a time such that
This is Theorem 1.1 of the source (p. 3), with the difference placed in the common interval of strong continuity, which is where the source establishes it. The goal is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. If the source's proof is correct, the theorem shows that the DiPerna–Lions framework, even with local mass conservation, momentum conservation and the energy and entropy inequalities retained, does not determine the evolution uniquely. The example is spatially inhomogeneous and periodic, and the two solutions start from exactly the same datum, unlike ill-posedness results that compare nearby data. On the interval where they differ, both solutions satisfy the unrenormalized equation. The datum has bounded velocities but unbounded amplitudes concentrated at smaller and smaller spatial scales, which points to the kind of extra control a uniqueness theorem has to impose.
Formalizing it. The statement fixes a long list of admissibility conditions. Its definitions are a useful contribution in their own right: renormalized solutions, entropy dissipation and kinetic test functions on the torus are not in Mathlib. The 65-page proof (colored decompositions, Carleman representation, velocity averaging, a dilation limit and a branching analysis) is a long-term target. Its propositions are natural milestones.
Constructing two different weak limits is not the hard part: approximations with and without a small "hot seed" give two candidate solutions. The difficulty is to show that they really differ. A vanishing seed can produce a hit on the a priori cap that carries arbitrarily little mass, and weak compactness can erase it in the limit. The source must rule out this loss of information uniformly as the cold velocity distributions collapse onto an axis, where the weight controlling the hot density is singular. At the same time every admissibility condition, including the entropy-dissipation inequality and local mass conservation, has to survive the limits. Energy-increasing constructions (Wennberg) and homogeneous examples do not meet these constraints.
EuclideanSpace ℝ (Fin 3), positions in Fin 3 → AddCircle 1, and densities are real functions on phase space. The sphere carries (volume).toSphere, which is ordinary surface area, not a probability measure.gain and loss are Bochner integrals. To prevent them from silently returning on non-integrable fibers, AdmissibleGlobal requires fiberwise integrability and space-time integrability of the renormalized gain and loss.AdmissibleGlobal f₀ F encodes Definition 2.1: finite entropy at each time, a.e. initial value, weak continuity against bounded measurable tests, uniform moment bounds, the renormalized equation for all Renormalization and all smooth periodic KineticTest , local mass conservation against MassTest, total momentum conservation, the energy inequality, and the entropy inequality in ℝ≥0∞ with the lower semicontinuous extension of .StrongEarly T F adds , strong continuity on via eLpNorm, and integrability of gain and loss on . Distinctness is ¬ (F t =ᵐ G t) for some .Purely infinite -algebras are the infinite counterpart of the finite, tracial algebras: every positive element can absorb copies of itself. In the simple case they are the Kirchberg algebras, classified by K-theory. For non-simple algebras, Kirchberg and Rørdam introduced three versions of pure infiniteness (weak, ordinary, strong) and showed that the strongest one is equivalent, for separable nuclear algebras, to absorbing the Cuntz algebra tensorially, the regularity property that underlies Kirchberg's classification of non-simple purely infinite algebras. Whether the three notions coincide is Kirchberg–Rørdam's Question 9.5, listed as Problem LXXII by Schafhauser, Tikuisis and White.
The source of this mission is an OpenAI preprint dated September 25, 2026, which proves ordinary strong in general and weak ordinary for exact algebras.
All -algebras are complex and may be nonunital or nonseparable. For positive in matrices over (or in ), write (Cuntz subequivalence) if there are with in norm; matrices of different sizes are compared after zero padding. A positive is properly infinite if (zero counts as properly infinite). The paper uses two conditions:
is strongly purely infinite if for all and there are with
is exact if preserves short exact sequences of -algebras.
If satisfies (P), then for all , , there are with
in particular is strongly purely infinite.
The Lean statement OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite is open on the platform.
Theorem 1.1 answers the ordinary-to-strong part of Problem LXXII for arbitrary algebras, and Theorem 1.2 answers the whole comparison question for exact (hence for nuclear) algebras. With Kirchberg's results, every separable nuclear algebra satisfying () absorbs (Corollary 1.3), with no unitality or simplicity assumption: a single finite amplification test characterizes this tensorial regularity. The weak-to-ordinary implication for non-exact algebras remains open.
These results are stated in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proofs exist.
For non-simple algebras, comparing one positive element with itself and comparing two elements simultaneously are different demands: strong pure infiniteness must also kill a mixed entry , and earlier proofs needed control of the ideal structure (Hausdorff primitive spectrum, ideal property, topological dimension zero). Removing a fixed amplification similarly needs enough orthogonal equivalent pieces in hereditary subalgebras, which earlier work extracted from Global Glimm-type hypotheses. The difficulty is to obtain this uniformly over primitive quotients when is not Hausdorff.
NonUnitalCStarAlgebra with the order (StarOrderedRing); no unit, separability or simplicity is assumed.CStarMatrix blocks, witnessed by rectangular matrices with for every ; is diagonalCopies n h; WeaklyPurelyInfinite fixes one before quantifying over nonzero positives.Exact is stated with minimal tensor products realized inside over all pairs of Hilbert-space representations, and tests surjections in the same universe.PropertyP is (P).StronglyPurelyInfinite is the three-inequality condition above, with no norm bound on .A complete development needs Cuntz comparison, stabilizations, minimal tensor products and exactness, primitive ideal spaces and hereditary subalgebras; this is reusable for other regularity missions. Contributions formalizing Proposition 2.2-style transport lemmas and Corollary 1.3 (via Kirchberg's absorption theorem) are welcome.
The word problem for a group with a finite generating set asks whether a given word in the generators and their inverses represents the identity; it is decidable if one algorithm answers this for every word. Since Higman's embedding theorem (1961), a recurring theme in combinatorial group theory has been to characterize algorithmic properties of groups by embeddings into groups with good algebraic properties. Boone and Higman (1974) proved that a finitely generated group has decidable word problem if and only if it embeds in a simple subgroup of a finitely presented group, and asked whether the simple group can itself be taken finitely presented. This is the Boone–Higman conjecture.
This preprint states a proof of the conjecture: a finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.
A group is finitely generated if some finite tuple generates it. A word is a finite list of letters ; has decidable word problem if for some finite generating tuple the set of words evaluating to is computable. A group is finitely presented if it has a presentation with finitely many generators and relations, and simple if it is nontrivial with no normal subgroups other than and itself. An embedding is an injective homomorphism.
In Lean (OAI.FiniteAlgebraicEnvelopes, definitions BooneHigman), words are List (Fin n × Bool), evalWord multiplies generators or their inverses, HasDecidableWordProblem G asserts a generating tuple whose identity predicate is ComputablePred, and EmbedsInFinitelyPresentedSimpleGroup G asserts a group in the same universe that is Group.IsFinitelyPresented and IsSimpleGroup, with an injective homomorphism from .
For every finitely generated group ,
The implication from right to left is classical (a finitely presented simple group has decidable word problem, and the property passes to finitely generated subgroups); the content is the forward implication.
The result. Theorem 1.1 gives a purely algebraic characterization of decidability of the word problem and settles a question open since 1974. Its intermediate result, Theorem 1.2, embeds every finitely generated group with decidable word problem in a finitely presented group with a faithful two-transitive action on a countably infinite set with finitely generated point stabilizers, which feeds Zaremsky's criterion for twisted Brin–Thompson groups.
Formalizing it. No machine-checked proof exists, and the source is an unrefereed preprint. Formalizing it requires computability of word problems, finite presentations (available in Mathlib as Group.IsFinitelyPresented), Steinberg groups over noncommutative rings, and twisted Brin–Thompson groups, which are not in Mathlib. The proof also uses Zaremsky's finite-presentation theorem (Theorem 2.3) from the literature, which a complete formalization must include.
Finite presentation does not pass to subgroups, so Boone and Higman's simple group and finitely presented group cannot simply be merged. Thompson's construction gives a finitely generated simple overgroup but provides no finite presentation. The new route needs a finitely presented group acting faithfully and two-transitively, built from a finitely presented algebra whose simplicity appears only after passing to a direct limit, and an exact calculation removing the kernel of the Steinberg group without assuming it is central.
GroupType : Type u with [Group GroupType] [Group.FG GroupType]; the target group lives in the same universe.ComputablePred on words over a specified finite generating tuple (Subgroup.closure (range generators) = ⊤); since the word problem's decidability is independent of the finite generating set, this matches the source.IsSimpleGroup includes nontriviality, matching the paper's convention.The statement is not trivially true: both directions are required for every finitely generated group, including infinitely presented ones.
Needed infrastructure: computable group presentations, Steinberg groups, mapping tori of endomorphisms, twisted Brin–Thompson groups and Zaremsky's criterion. Contributions toward the classical backward implication, or toward Theorem 1.2, are welcome.
The Hadwiger–Nelson problem asks for the chromatic number of the plane : the least number of colours needed to colour every point of the Euclidean plane so that any two points at distance exactly receive different colours. Equivalently, it is the chromatic number of the infinite graph whose vertices are the points of the plane and whose edges are the unit-distance pairs. Since 1950 the answer has been known to lie between and , and it is one of the best known open problems in combinatorial geometry. Its difficulty is that the colour classes may be arbitrary sets: no measurability or regularity is assumed, so analytic tools that work for measurable colourings do not apply directly.
This mission asks for a formal proof that five colours do not suffice, as claimed in an OpenAI preprint dated September 23, 2026 (source), so that . The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
A proper -colouring of the plane is any function such that whenever , with the Euclidean norm. No measurability, continuity or regularity of the colour classes is assumed. is the least admitting a proper -colouring.
There is a proper -colouring of the plane: colour the Voronoi hexagons of a triangular lattice (circumradius ) by the seven cosets of an index-seven similar sublattice, assigning boundary points to any incident hexagon. This classical construction is reproved in the deduction of Theorem 1.1 (pp. 2–3), including all boundary points.
There is no function with whenever . Together with the milestone this gives .
The result itself. It raises the lower bound for the chromatic number of the plane from five (de Grey, 2018) to six, leaving only and . Unlike de Grey's bound it is not witnessed by a finite graph; the proof transfers the problem to measurable colourings for every number of colours (Theorem 1.3, p. 2) and then excludes weak measurable five-colourings (Theorem 1.4, p. 2). The transfer theorem is of independent interest: in ZFC, a proper -colouring exists iff a weak measurable -colouring does. The preprint also derives a positive lower bound on the invariant-mean frequency of monochromatic unit pairs for every five-colouring (Corollary 1.5, p. 5).
Formalizing it. The statements are elementary, but the proof uses ergodic theory (a Furstenberg–Zimmer compact-extension tower and rigidity of invariant measures on a character group, Theorem 2.3, p. 6), spectral theory, density points, Fourier decay of circle measure, and planar topology. A formal proof would remove any doubt about a long and varied argument. The finite-graph bound has been checked by SAT solvers, but no formal proof of a bound that is not witnessed by a finite graph is known.
By de Bruijn–Erdős, is equivalent to the existence of a finite unit-distance graph that is not -colourable, but no such graph is known, and SAT-based searches have not produced one. Measurable methods (Falconer's density-point argument) cannot be applied to arbitrary colour classes, and a measurable colouring can have boundaries far too irregular for map-type interface arguments such as Townsend's or Sokolov–Voronov's. The preprint must therefore (i) produce measurable data from an arbitrary colouring without losing the unit-distance exclusions, via invariant averaging over algebraic rotations and translations and the rigidity Theorem 2.3, and (ii) construct the connected interfaces needed for a geometric contradiction from measure estimates alone (Sections 5–7), before excluding label cycles of length , and (Section 8).
ℂ with ‖p - q‖ = 1; a colouring is any function ℂ → Fin 5. ProperColoring 5 c requires distinct colours at every unit-distance pair. No measurability is assumed, so the statement is about arbitrary colourings, as in the source.EuclideanSpace ℝ (Fin 2) with dist x y = 1 and asks for some c : Plane → Fin 7; the two planes are isometric.Welcome contributions: the de Bruijn–Erdős compactness theorem, the Moser spindle, Lebesgue density points in , and the measurable/unrestricted transfer of Theorem 1.3.
A matroid abstracts linear independence: a finite ground set with a family of "independent" subsets that is closed under subsets and satisfies the augmentation axiom. Its maximal independent sets, the bases, all have the same size, the rank. Matroid intersection, finding a common basis of two matroids, is one of the central polynomially solvable problems of combinatorial optimization (Edmonds, 1979). Counting common bases is much harder. It contains counting bases of a single matroid (take both matroids equal) and counting perfect matchings of a bipartite graph (take two partition matroids), and exact counting is #P-hard. The natural goal is therefore a fully polynomial randomized approximation scheme (FPRAS): an algorithm whose output is within relative error with probability at least , in time polynomial in the input size, and . The matroids should be accessible only through independence oracles.
Let be matroids of the same rank on the ground set , supplied by exact independence oracles: a query is an -bit indicator of a subset, and the answer says whether it is independent. The quantity to estimate is
the number of common bases. The input also contains rationals ; denotes the binary encoding length of . Oracle calls are counted separately from the bit operations used to build queries and process answers.
There is a single randomized oracle algorithm and a fixed polynomial such that, for all rank- matroids on and rational , it outputs a nonnegative rational with
the output is always when , and on every execution the numbers of oracle calls and bit operations are at most . The algorithm uses only independent fair random bits. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 answers the question recorded by Liu (2023) and extends both the single-matroid FPRAS of Anari–Liu–Oveis Gharan–Vinzant and, in the bipartite-matching case, the permanent FPRAS of Jerrum–Sinclair–Vigoda. It needs no representation of either matroid and holds for unrestricted rank, whereas the previous oracle-model scheme was fully polynomial only for . The source derives FPRASs and almost-uniform samplers for common independent sets of prescribed, unrestricted or maximum size, even for matroids of different ranks (Corollary 9.1).
Formalizing it. The Lean goal fixes a concrete machine model, so it states a complete complexity-theoretic claim with no informal "polynomial-time" left. A proof would combine Lorentzian-polynomial inequalities (Brändén–Huh), a transport inequality, a Markov-chain Poincaré bound, and simulated annealing with explicit bit accounting. Each layer is reusable: Mathlib has matroids, but no Lorentzian polynomials, no mixing-time theory of this kind and no randomized-algorithm framework.
For one matroid, the bases-exchange walk mixes rapidly because the basis generating polynomial is log-concave. The intersection of two matroids has no such structure: its common bases need not be connected by short exchanges, and the natural chain on transversals of the paired construction passes through states of exponentially small weight, so positivity and connectivity alone give no polynomial bound. Earlier approaches either lost exponential factors or needed real-stable polynomials that an independence oracle does not provide. The proof must balance defect classes, as in Jerrum–Sinclair–Vigoda, and establish a Poincaré inequality for observables from matroid-theoretic inequalities alone.
Matroid (Fin n) with ground set univ and eRank = r for both. Oracles are functions Bool → (Fin n → Bool) → Bool, required to answer independence queries exactly.Program k s for a register machine with binary stacks: push/pop, fair coin, oracle query on an -bit register, and halt with output (register 6)/(register 7) as a rational. Inputs are loaded in binary.In the local model of differential privacy, each individual randomizes their own data before handing it to an untrusted learner. Local protocols are the deployed form of private data collection, and in practice every round of interaction with the population is expensive: the learner must broadcast new instructions and wait for new reports. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are those of arXiv v3) show that local learning is equivalent to learning with statistical queries (SQ) in the sense of Kearns (1998), and that the equivalence maps noninteractive local learners to nonadaptive SQ learners. The question whether interaction is ever necessary in the local model therefore becomes the question whether adaptivity is ever necessary for SQ learning.
This mission formalizes the paper's answer (§5.3, Theorem 5.16): a concept class, MASKED-PARITY, that an adaptive SQ learner learns exactly with queries in two rounds, while every nonadaptive SQ learner with fewer than exponentially many queries fails against a specific valid oracle, under the uniform distribution on examples.
Fix , a power of two. The domain is , with points , and examples are drawn from the uniform distribution on . For and , the concept is
where is the inner product modulo 2. MASKED-PARITY is the class : on the half it is the parity or its negation, according to the mask ; on the half it reveals the bit .
A statistical query is a function of an example and a label together with a tolerance . The SQ oracle for the target answers with any real such that ; the learner must succeed for every such answer. An SQ learner is nonadaptive if it fixes all its queries before receiving any answer, and adaptive otherwise. Write and .
The lower bound uses the decomposition of a query into and , the restrictions , of and to the half (equation (6)), and the oracle
The result. Combined with the paper's equivalence between local and SQ learning (Theorem 5.14), Theorem 5.16 shows that interaction is sometimes necessary in local differential privacy: there is a class learnable by an interactive local protocol with polynomially many examples, but not by any noninteractive one with fewer than exponentially many (Corollary 5.17). The separation concerns strong learning under a fixed distribution; the paper notes that adaptive and nonadaptive SQ learning coincide for weak learning, and that a distribution-free separation was left open.
Formalizing it. The result is proved in the paper and has, to our knowledge, no machine-checked proof. The mission produces a self-contained Lean model of statistical query learning with labelled queries and adversarial oracles, a finite Fourier calculus for parities on (orthogonality and a Bessel inequality for -valued functions), and the counting and union-bound argument of SQ lower bounds. The proof of part (2) contains several printed slips (listed below); a formal proof settles the corrected argument.
The upper bound is a direct computation. The difficulty is in part (2): the learner's hypothesis may be any function, not a concept of the class, and the lower bound must hold for every nonadaptive strategy at once. A naive argument that each query "reveals little about " fails, because the true answer to a query does depend on ; the argument needs an oracle that is valid (within tolerance of the truth) and yet independent of on most targets, and a quantitative bound on how many targets any single -valued query can correlate with on the half . That bound is an statement over all concepts, not a pointwise one.
Fin d, and every theorem assumes (implicit in the paper). Vectors are Fin d → ZMod 2, with 0-based bits. Expectations are averages over the finite domain; probabilities over the target are counts of pairs divided by .Contributions welcome: the Fourier facts for (reusable for any parity-based SQ lower bound), the general decomposition (7), and the probability bound of part (2) from the milestones.
Matrix-valued affine processes on the cone of positive semidefinite matrices are used in finance as models of stochastic covariance: multi-asset option pricing with stochastic volatility and correlation, and fixed-income models with stochastically correlated risk factors and default intensities. The best-known example is the Wishart process of Bru (1991). What makes these models tractable is that the Laplace transform of the state is exponential-affine in the initial state, with exponents that solve ordinary differential equations of Riccati type.
Cuchiero, Filipović, Mayerhofer and Teichmann (2011) give the mathematical foundation: a complete characterization of stochastically continuous affine processes on through an admissible parameter set. Their Theorem 2.4 has two halves. This mission formalizes the first, necessity, half: every affine process on is regular and Feller, and its generator and Riccati equations are given by an admissible parameter set.
Timeline. Duffie, Filipović and Schachermayer (2003) characterized regular affine processes on the canonical state space , assuming regularity. Keller-Ressel, Schachermayer and Teichmann showed that on that state space stochastic continuity already implies regularity. The 2011 paper carries both the characterization and the regularity result over to , a non-polyhedral cone with a curved boundary, on which the drift must satisfy the new condition .
Let be the space of real symmetric matrices with scalar product and norm . Let be the cone of positive semidefinite matrices and its interior, and write when .
A time-homogeneous Markov process on is described by sub-stochastic transition kernels , . Mass that is lost goes to a cemetery state . The kernels satisfy the Chapman–Kolmogorov equations, and the semigroup is . The process is affine (Definition 2.1) if it is stochastically continuous, i.e. weakly as , and if there are and with
It is regular (Definition 2.2) if and exist and are continuous at .
An admissible parameter set , associated with a bounded continuous truncation function (equal to the identity near ), consists of:
These are subject to the boundary conditions (2.9) and (2.11) for with . The space consists of restrictions to of rapidly decreasing smooth functions on .
If is affine on , then is regular and Feller, lies in the domain of its generator on , and there is an admissible parameter set such that for
with . In addition, solve , , , , with
The result. Theorem 2.4 reduces the study of affine processes on to finitely many parameters. Any such process, a priori specified only through its Laplace transform, has the Lévy–Khintchine-type generator (2.12), its Laplace exponents solve the Riccati system, and its parameters obey the admissibility conditions. The drift condition is the matrix analogue of the Feller condition, and for it excludes affine diffusions on with zero constant drift. The Feller property yields càdlàg versions, and the generator formula is the starting point for the semimartingale description and for the converse existence result.
Formalizing it. The theorem is proved in the paper, and this mission produces a machine-checked version of the necessity direction. Along the way it builds reusable infrastructure: a Lean model of Markov transition families on a cone, Feller semigroups on of a closed cone, generators on Schwartz-type test spaces with the symmetric-matrix derivative convention, and the positive semidefinite cone's order and boundary facts. No machine-checked proof of this theorem, or of its predecessor, is known to exist.
The definition assumes only stochastic continuity and the exponential-affine form of the Laplace transform; differentiability in time is not given. Obtaining regularity, and hence the Riccati equations, needs the positivity statement of Lemma 3.3. Its proof uses analyticity in and the boundary geometry of . Identifying and requires Lévy–Khintchine representations on cones and on , and a convergence theorem for Laplace transforms. The admissibility conditions on the boundary come from support considerations at each boundary point. The drift condition (2.4) is not captured by the conditions read off from Laplace exponents at boundary points along single directions; it is a genuinely matrix-valued constraint coupling and . Extending the generator formula from exponentials to all of needs a density result in a Fréchet topology and the closedness of the generator.
Fin d → Fin d → ℝ, with and . Mathlib's positive semidefiniteness, which includes symmetry over , defines . The state space is the subtype with its subspace topology and Borel -algebra.EthierKurtz.IsStronglyContinuousContractionSemigroup on . " and " is uniform convergence of to on .Noisy low-rank matrix completion asks to reconstruct an matrix from noisy observations of randomly chosen entries. It is the statistical model behind collaborative filtering (recommender systems), sensor localization and system identification, and the nuclear-norm penalized least-squares estimator is its standard convex method. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4, Ann. Statist. 2011) proved sharp oracle inequalities for this estimator and showed that its Frobenius error is of order up to normalization, which matches the minimax lower bound up to a logarithmic factor.
An upper bound alone does not say whether the estimator really attains this rate on a given matrix, nor whether it reports the correct rank. Section 5.1 of the paper answers both questions with a single deterministic theorem, Theorem 8: with a slightly inflated regularization parameter the estimator never overestimates the rank of ; if the nonzero singular values of are separated from zero it recovers the rank exactly, and its error is then bounded below by a quantity of the same order as the upper bounds. Rank recovery is the property practitioners rely on when they use the estimator for model selection (choosing the number of latent factors). This mission formalizes Theorem 8 and the steps of its proof.
Fix integers . The matrix completion basis is , the matrices with a single entry equal to . A sample consists of pairs with (an observed position ) and (a noisy observation of the corresponding entry of the unknown matrix ). Write , for the Frobenius norm, for the nuclear norm (the sum of the singular values) and for the operator norm (the largest singular value). The singular values of are .
From the sample form
In the paper's model with uniform on , so and : the matrix is the stochastic error. For the estimator (3.1) is
The objective is strictly convex, so the minimizer is unique; by (3.2) it is obtained from a singular value decomposition of by soft thresholding every singular value at level .
Let , and , and put . Then
If in addition , then
and
The milestones follow the proof on p. 20 in order:
The result. Theorem 8 turns the paper's upper bounds into two-sided statements. Combined with a probability bound for (Corollary 3 of the paper), it shows that with high probability the estimator selects the true rank and that its error on well-conditioned low-rank matrices is not smaller than the rate of the upper bounds, so those bounds cannot be improved for this estimator. Because the theorem is deterministic given the event , it applies unchanged to any noise model for which such a bound on the stochastic error is available.
Formalizing it. The theorem is proved in the paper; nothing in it is open. The mission produces a machine-checked version and, along the way, reusable linear algebra that is not on the platform in this form: Weyl's perturbation inequality for singular values in operator norm, the rank of a nuclear-norm proximal point, and the Frobenius norm of a projection onto a span of orthonormal rank-one matrices. The soft-thresholding representation (3.2) itself is the open platform item CaiCandesShen.Convergence.shrink_eq_prox (Cai–Candès–Shen, Theorem 2.1, after halving the objective); this mission references it rather than posing it again, and a proof of it would serve both missions.
The arithmetic of the proof is three lines; the content is in two facts about singular values that the paper takes from the literature. The first is Weyl's inequality , which needs the min–max (Courant–Fischer) characterization of singular values; Mathlib defines singular values through the eigenvalues of but has neither the min–max principle for them nor this inequality. The second is the description of the minimizer of : one needs the subdifferential of the nuclear norm (2.1), or an equivalent von Neumann trace inequality, to show that soft thresholding is optimal, and then that its rank and its projection onto the top singular pairs are what the formula suggests. A naive approach that compares the estimator with entrywise gives nothing about the rank; the proof needs the spectral structure.
Matrices are MatrixCompletion.RealMatrix m₁ m₂ (Matrix (Fin m₁) (Fin m₂) ℝ) with the published norms frobeniusNormSq, frobeniusNorm, nuclearNorm, spectralNorm and SVD data SVD. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin, 0-based: the Lean singularValue B j is the paper's . The conventions committed to:
idx : Fin n → Fin m₁ × Fin m₂ and responses y : Fin n → ℝ are fixed, and every theorem holds for every data set satisfying . The matrix is written as , which is (2.2) under the model (1.1) and the uniform design; this is the paper's "Note that ". The probabilistic hypotheses are used for nothing else.No printed slip was found in Theorem 8 or its proof; no hypothesis beyond the above is added.
Contributions welcome: Weyl's inequality for singular values (generally useful), the rank and top- projection of the nuclear-norm proximal point, and a proof of CaiCandesShen.Convergence.shrink_eq_prox.
The source is the arXiv preprint arXiv:1011.6256v4; all page and display numbers refer to it.
Backward stochastic differential equations (BSDEs) describe the price and the hedge of a contingent claim in models with nonlinear pricing rules (differential interest rates, funding costs, reflected or constrained claims), and give probabilistic representations of semilinear parabolic PDEs (El Karoui, Peng and Quenez, 1997). Their numerical solution in moderate dimension is done by simulation: a backward recursion over a time grid in which each conditional expectation is replaced by a least-squares regression on simulated paths, the same device as the regression method for Bermudan options of Longstaff and Schwartz (2001).
Gobet, Lemor and Warin (2005) split the error of such a scheme into three parts: time discretization (Theorem 1), projection on finite function bases (Theorem 2), and the replacement of projections by empirical regressions on simulated paths (Theorem 3). This mission formalizes the third part, which the authors describe as the major contribution of the paper. Its point is that the error from the simulations is controlled nonasymptotically, step by step, without blowing up as the time step shrinks, even though every regression of the backward recursion reuses the same simulated paths.
A model consists of a horizon , a drift , a diffusion satisfying the Lipschitz condition (H1), and a driver satisfying (H2): . For , , , the Euler scheme is , where the increments are independent of the past. A chain extends , and is the terminal value.
At each time , function bases (for ) and , (for the components of ) are fixed, orthonormal in the sense . The projection–Picard scheme (Definition 1) computes coefficients by Picard iterations of an least-squares problem, and sets , .
The empirical scheme (4) replaces the expectation by an average over independent simulations of the path: minimizes
The outputs are truncated: with and a smooth profile equal to the identity on , with . The regression vector is , and the good event (27) asks that the empirical matrices and be close to the identity for all .
For , orthonormal bases with , such that the bounds of Proposition 2 hold, and small enough, for ,
where collects second moments of , and , written out in full in the goal statement. The constant and the threshold on depend only on the model and on .
Theorem 3 is nonasymptotic: together with Theorems 1 and 2 it lets one compare the three error sources and choose , the bases and jointly for a target accuracy. The rate shows how many paths a finer time grid requires, and the term shows that Picard iterations suffice. The term involving isolates the event on which the empirical regression matrices are badly conditioned, which the truncation keeps under control.
The result is proved in the paper; nothing in this mission is open mathematically. No machine-checked proof of any part of it is known. A formal proof would check a long chain of estimates whose constants the paper tracks only as a generic , and would settle the two misprints in the printed statement (see below). The definitions layer (Euler scheme, regression schemes, empirical regression matrices) is reusable for other regression Monte Carlo schemes for BSDEs and for optimal stopping.
The obvious approach is to treat each regression as an independent statistical estimation problem and apply a variance bound per time step. This fails because all regressions of the backward recursion use the same paths: the response at time is itself a function of the simulations, so the regression at is not a regression of a fixed variable on independent samples. Moreover, the empirical matrix may be singular, and on that event the empirical coefficients are unbounded unless truncated. A naive per-step bound also produces a factor at each of the steps, which explodes; the proof must keep the accumulated constants of order one.
RegMCBSDE.Simulation. Continuous time is not used: the increments are any family that is -measurable, independent of and -distributed for some filtration. That covers the Brownian case. (H3), a condition on the terminal functional of the continuous path, is dropped. So is the Markov representation of , which no statement uses.Contributions welcome: proofs of the milestones, in particular (28)–(29) (finite-dimensional linear algebra) and (34) (independence and orthonormality), and a construction showing that measurable minimizers of (4) exist.
Many estimation problems ask for a low-rank matrix from far fewer linear measurements than it has entries: matrix completion, quantum state tomography, recovery of positions from partial distances. The rank minimization problem subject to is NP-hard, so one solves a tractable surrogate instead, either the nuclear-norm minimization subject to or an iterative scheme such as the iteratively reweighted least squares algorithm IRLS-M of Fornasier, Rauhut and Ward (arXiv:1010.2471).
Guarantees for these surrogates rest on conditions on the measurement map. Two are standard. The restricted isometry property (RIP) asks that nearly preserve the Frobenius norm of every low-rank matrix; it holds with high probability for many random maps, and it is what one can verify in practice. The null space property asks that no nonzero matrix in the kernel of be concentrated on few singular directions; it is what the recovery proofs actually use. This mission formalizes the bridge between them in the paper's form: a small restricted isometry constant implies the strong rank null space property (SRNSP) that drives the convergence analysis of IRLS-M.
Timeline.
Fix integers . A measurement map is a linear map ; it is given by matrices through , where . The Frobenius norm is , the nuclear norm is the sum of the singular values of , and is the Euclidean norm of the vector . A matrix is -rank if its rank is at most .
The restricted isometry constant (Definition 1.1) is the smallest such that
The map has the strong rank null space property of order with constant (Definition 6.4) if for every and every decomposition with -rank, there is another decomposition with , , , , and
In Lean these are IRLSM.RIP.ripConst A k, IRLSM.RIP.SRNSP A k η and IRLSM.RIP.measSq A X , built on the published module HighDimStat_MatrixRank_Core (traceInner, frobeniusNorm, nuclearNorm, observationOp).
If and
then satisfies the SRNSP of order with constant
The constant is the paper's explicit one; the goal asserts the full property for every kernel element and every decomposition, including .
The result. Proposition 6.8 is the step that turns a verifiable, probabilistically typical hypothesis (a small rank restricted isometry constant, which Gaussian and many other random maps satisfy once is of order ) into the deterministic null-space hypothesis under which the paper proves that IRLS-M converges to the nuclear-norm minimizer and recovers every -rank matrix exactly (Theorem 6.11, Proposition 2.1). Through Lemma 6.6 and Corollary 6.7 of the same paper, the SRNSP also gives stable recovery by nuclear-norm minimization, with error controlled by the best -rank approximation error in the nuclear norm.
Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. A complete development supplies the rank restricted isometry constant as a usable object (its monotonicity, its polarization estimate Lemma 6.9), the nuclear norm's additivity on orthogonal pieces, its comparison with the Frobenius norm, and the block-splitting of the singular value decomposition. These tools are reusable across low-rank recovery. The sibling mission of this series, IRLS-M Converges to the Nuclear-Norm Minimizer Under the Strong Rank Null Space Property, takes the SRNSP as its hypothesis; together the two give Proposition 2.1 of the paper.
The obvious argument would bound directly by the restricted isometry inequality, but that inequality controls only Frobenius norms of low-rank matrices, while the kernel element has full rank in general and the property is stated in nuclear norms. The restricted isometry hypothesis therefore cannot be applied to , or to , as a whole, and the constant depends on how the high-rank part is handled. In Lean, the singular value decomposition of a rectangular matrix and the behaviour of singular values under block operations are the main missing infrastructure: Mathlib has the spectral theorem for Hermitian matrices but little on singular values of rectangular matrices.
Matrix (Fin n) (Fin p) ℝ; the paper treats real and complex matrices indifferently. is and is traceInner.observationOp); is a sum of squares, not Mathlib's sup norm on Fin m → ℝ.n ≤ p assumption: the proof does not use it.A formalization that proved only , or only the existence of some decomposition without the bound , or that defined as any admissible constant rather than the smallest one, would not be this mission's goal.
Welcome contributions: singular value decomposition for rectangular real matrices in the Core encoding, singular values of block-diagonal and orthogonally-equivalent matrices, and proofs of the milestones in any order.
Network data often come as a single observed graph, and the simplest summary of a graph is its degree sequence, the list of the numbers of neighbours of its vertices. A statistical model in which the degree sequence is a sufficient statistic is an exponential family on graphs, and the simplest such family is the β-model: each vertex carries a parameter , and edges appear independently with log-odds . The model appears in the directed case in Holland and Leinhardt (1981), in the undirected case in Park and Newman (2004) and Blitzstein and Diaconis (2011), and it is a close relative of the Bradley–Terry model for paired comparisons.
Fitting the model means solving the maximum likelihood equations. The difficulty for classical theory is that the number of parameters, , equals the number of vertices: the parameter dimension grows with the sample, and standard consistency arguments for maximum likelihood do not apply. Chatterjee, Diaconis and Sly (2011) prove that, nevertheless, for parameters in a fixed bounded range the maximum likelihood estimate exists, is unique, and estimates every coordinate of uniformly at rate , with probability . This mission formalizes that result (Theorem 1.3 of the paper) and the lemmas of §4 on which its proof rests.
Let and . The β-model is the law of the random simple graph on vertices in which, for each pair , the edge is present with probability
independently of all other edges. Write for the degrees of . The maximum likelihood equations for an estimate are
The sup norm is .
Two further objects enter the proof. is the set of degree sequences of simple graphs on vertices and the set of expected degree sequences of as ranges over . For and the slack is
which is nonnegative for every degree sequence of a graph (the Erdős–Gallai inequalities). Finally , , is the map whose fixed points are the solutions of (3).
For every there is such that for every and every with ,
The constant depends only on , and the statement holds for all , small being absorbed into .
The theorem is a consistency result in a regime where the number of parameters is as large as the number of nodes, and it comes with a uniform rate: every vertex parameter is recovered to accuracy simultaneously, from one graph. Existence of the MLE is itself not automatic (it fails, for instance, whenever the observed graph has an isolated vertex), so the theorem also says that the estimator is defined with high probability. The paper uses the same machinery for its graph-limit results on uniform random graphs with a given degree sequence (missions 4–5 of this series), and the β-model is the base case of a large family of exponential random graph models used in network analysis.
The result is proved in the paper; this mission produces the machine-checked version. None of the statements here is formalized on the platform or in Mathlib. Theorems 1.4 and 1.5 are the goals of missions 2 and 1 of this series and are restated here; a proof there transfers directly.
Standard maximum likelihood asymptotics fix the parameter dimension and let the sample size grow; here both grow together, and the ratio of squared dimension to number of observations, , stays bounded, so the usual heuristic for when asymptotics apply is borderline at best. The likelihood is concave, but concavity alone gives neither existence of a maximizer (the supremum may be approached at ) nor a bound on its size that is uniform in . The central step, Lemma 4.1, is a deterministic bound on that does not depend on ; it requires control of how the coordinates of can spread out, expressed through a quantitative Erdős–Gallai margin. A coordinatewise argument cannot give it, because each equation of (3) involves all coordinates.
Vertices are Fin n, graphs are SimpleGraph (Fin n) with the discrete σ-algebra, and is the finite sum of point masses with the independent-edge weights ; vectors are Fin n → ℝ with Mathlib's sup norm. Probabilities are values of this measure in , compared with . Expected degrees are integrals against ; is not defined as the range of the right-hand side of (3), since that identification is part of the content of Theorem 1.4.
Every "constant depending only on …" is a quantifier placed before : in Theorem 1.3, depends on only; in Lemma 4.1, is a function of alone, bounded on compact subsets of its domain, as §4 defines the phrase; in Lemma 4.2, on and on . Choosing after and would make Theorem 1.3 trivial, since for large ; this formalization rules that out. The paper's is the hypothesis , and the paper's is the bound for every admissible (a finite nonempty family). The phrase "there exists a unique solution … that satisfies [the bound]" is read as: a solution exists, it is unique, and it satisfies the bound. Lemma 4.1 assumes , not (for existence would be immediate). Theorem 1.5 is stated, as in mission 1, for and .
A complete development needs: the β-model as a measure and its exponential-family formula; Hoeffding's inequality for sums of independent non-identical indicators transported to (Mathlib has Hoeffding for independent bounded variables); compactness in ; and the results of missions 1 and 2. The β-model measure and the Erdős–Gallai slack are reusable beyond this mission. Proofs of any milestone, and of the transfer between the independent-edge and the product-space descriptions of , are welcome.
A standard way to build a random network with a prescribed degree sequence is to choose a graph uniformly at random from the set of all simple graphs with that degree sequence. The model arises in testing whether the exponential family with the degree sequence as sufficient statistic fits network data, in simulating networks with given degrees, and, for constant degrees, as the random regular graph (Blitzstein–Diaconis, Chatterjee–Diaconis–Sly). Quantities such as the expected number of triangles of such a graph are usually estimated by simulation.
For dense graphs, those whose number of edges is of order , the Lovász–Szegedy theory of graph limits (Lovász–Szegedy 2006) describes a large graph by a symmetric function . Chatterjee, Diaconis and Sly identify this limit for uniformly random graphs with a given degree sequence. The answer is the limit of the β-model, a random graph with independent edges whose edge probabilities are . The limit gives exact asymptotic formulas for subgraph counts without simulation.
Graphs and densities. For a finite simple graph on and a simple graph on vertices, the homomorphism density is
where is the set of edge-preserving maps . For ,
with one factor per edge. Graphs on vertices converge to the limit represented by if for every finite simple graph .
Degree sequences and scaling limits. For each let be the degree sequence of some simple graph on vertices. The sequence has scaling limit , a nonincreasing function on , if
is the set of nonincreasing functions on that are left continuous on . It carries the modified norm . is the set of all scaling limits of degree sequences.
The random graphs. is chosen uniformly from the simple graphs on with degree sequence . In a random graph with independent edges each pair is an edge with probability , independently of the other pairs. The β-model is the case .
If lies in the interior of for , there is a function , unique on , such that
and almost surely for every finite simple graph .
The proof also uses three results posed in sibling missions of this series: Proposition 1.2 (mission 4, the interior of ), Lemma 4.1 (mission 3, existence and boundedness of the MLE) and Theorem 1.5 (mission 1, geometric convergence of the iteration ). They are not restated here.
The theorem turns questions about a uniformly random graph with given degrees, a law with no independence, into questions about an explicit graphon. Every subgraph density, the limiting degree distribution, and every graph parameter continuous for the graph-limit topology of the uniform model is computed from . The function solves a continuum version of the β-model maximum-likelihood equations, which connects the combinatorial model with exponential-family statistics.
The result is proved in the paper, which is published in the Annals of Applied Probability (2011). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean development of dense graph limits (homomorphism densities, graphon densities, graph-limit convergence), none of which exists in Mathlib. It also requires a bounded-differences concentration inequality, and a transfer argument from independent-edge models to models conditioned on degrees. Each of these is reusable beyond this mission.
The uniform measure on graphs with a fixed degree sequence has no independence, so concentration inequalities do not apply to it directly. The obvious route is to condition an independent-edge model on its degree sequence. This works only if the probability of the conditioning event is larger than the concentration bound, which is . A crude lower bound of is too small. Lemma 6.2 supplies , and it needs a combinatorial completion step (Claim 6.3).
The second difficulty is analytic. The maximum-likelihood parameters for different live in different dimensions. One must show that their step-function profiles converge in to a limit and that this solves the continuum equation at every point of , not only almost everywhere. Several steps of the paper's argument are only sketched. Among them are the almost-sure convergence of the β-model graphs to and the estimate (pp. 33–34).
Fin n (the paper's vertex is ), graphs are SimpleGraph (Fin n), and a test graph is a SimpleGraph (Fin k), which loses nothing because densities are invariant under relabelling.ℝ → ℝ, and only their values on matter. Uniqueness of is equality on .SimpleGraph (Fin n) is discrete.A formalization that replaces almost-sure convergence by convergence in expectation or in probability, that fixes a single coupling, or that asserts the existence of only almost everywhere states a weaker theorem and does not close this mission.
Welcome contributions include a general graph-limit library (densities, convergence, the counting lemma), McDiarmid's bounded-differences inequality for finitely many independent Bernoulli variables, the Gale–Ryser theorem in the form needed by Claim 6.3, and proofs of the milestones.
Principal component analysis finds the best low-rank approximation of a data matrix, and it is used everywhere data come as a table: images, video, genomics, web and survey data. Its weakness is well known: a single grossly corrupted entry can move the classical principal components arbitrarily far. In many applications the corruptions are not small noise but gross errors at a fraction of the entries: occlusions and specularities in face images, moving foreground objects in surveillance video, corrupted or adversarial records. Robust variants of PCA built on robust statistics or on alternating heuristics came without guarantees of exact recovery.
Candès, Li, Ma and Wright (J. ACM 58(3), 2011) showed that a single convex program recovers both the low-rank part and the corruptions exactly, under a randomness assumption on the corruption pattern only, with a weight that needs no tuning.
Timeline.
Let have rank and compact singular value decomposition with , where and have orthonormal columns. The nuclear norm is the sum of the singular values of , and is the entrywise norm. Given , Principal Component Pursuit (PCP) solves
PCP is exact when is its unique solution.
satisfies the incoherence condition with parameter when
where . This excludes low-rank matrices that are themselves sparse, which no method could tell apart from corruptions.
The sparse component is , where is an arbitrary fixed matrix and keeps the entries in a random support and zeros the others. In Theorem 1.1, is uniform among all subsets of of cardinality . In the Bernoulli model each entry belongs to independently with probability . Nothing is assumed about the magnitudes or signs of .
The proof works with the tangent space of the rank- matrices at , its orthogonal projections and , and the operator norm (largest singular value).
There are positive numerical constants such that, whenever obeys (1.2)–(1.3) and
PCP with is exact with probability at least over the support of .
The constants are not specified, so the goal survives any improvement of them.
They are listed in the order the proof uses them:
The result. Theorem 1.1 is the founding guarantee of robust PCA by convex optimization. It allows a constant fraction of arbitrarily large corruptions and a rank as large as , with a universal weight . It supports applications such as background modeling in video and the removal of shadows and specularities from face images, and it is the template for later work on noisy and partially observed variants, e.g. stable PCP (Zhou et al., ISIT 2010, arXiv:1001.2363).
Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. A formal proof would check a chain that combines convex duality for the nuclear and norms, operator concentration for random sampling, and a probabilistic coupling. The reusable parts are general: the elimination and derandomization arguments, the certificate lemmas, the golfing scheme and the Bernoulli-to-uniform transfer. They also serve matrix completion and other sparse-plus-low-rank problems. The matrix-completion definitions this mission builds on are already published on the platform.
The obvious plan is to write down the subgradient optimality conditions of (1.1) and exhibit a dual certificate. The difficulty is the exact certificate (2.3). It requires exactly, and at the same time and , with a constant fraction of all entries. The natural least-squares candidate cannot be controlled in the sup norm on by moment methods at this sparsity level.
A second difficulty is probabilistic. The theorem allows fixed, adversarial signs. The concentration tools need independence, which fixed signs do not give.
Finally, every step must hold uniformly with failure probability and with constants independent of , and .
All statements are for square real matrices RealMatrix n n. The rectangular sentences of the paper are not stated. The mission reuses the published matrix-completion definitions for the following objects:
SVD L0 r, with = signMatrix;The following conventions are fixed:
SVD L0 r with positive singular values, so . Every statement holds for every such decomposition.Trivializing formalizations are excluded. A constant chosen after would make the goal vacuous, so all constants come first. A non-strict "optimal" would make exactness much weaker, so exactness is strict. The values of are fixed before the support is drawn.
Contributions of any kind are welcome. Proofs of the deterministic milestones (Theorem 2.2, Lemmas 2.4 and 2.5, (2.4), (2.2)) are self-contained convex analysis and linear algebra. The concentration milestones need matrix Bernstein-type inequalities and operator concentration, which are reusable well beyond this mission.
A uniformly random simple graph with a prescribed degree sequence is a basic null model in network science, statistics and combinatorics: it is what a network "looks like" when nothing but its degrees is known. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) show that when the normalized degree sequences converge to a limiting profile , these random graphs converge almost surely to an explicit graph limit (their Theorem 1.1). That theorem has a hypothesis: must lie in the interior of the set of all possible limiting degree profiles. A hypothesis of that kind is only useful if it can be checked, and the paper's Proposition 1.2 supplies the check, in the form of a continuum version of the Erdős–Gallai criterion (Erdős and Gallai, Mat. Lapok 1960), the classical test for whether a list of integers is the degree sequence of a simple graph.
This mission formalizes Proposition 1.2 and the steps of its proof in §5 of the paper, together with the Erdős–Gallai criterion itself, which the paper cites and uses in both directions.
A degree sequence on vertices is a vector of nonnegative integers for which some simple graph (undirected, no loops, no multiple edges) on vertices has for every . Such sequences are written in nonincreasing order .
The space consists of the functions on that are nonincreasing and left continuous at every point of . It carries the modified norm
Suppose that for every a degree sequence on vertices is given. The sequence has scaling limit , a nonincreasing function on , if
The set consists of the that arise as scaling limits of degree sequences. Its interior is taken in with the topology of : is interior if every with lies in , for some .
For and the paper defines
At , approximates the slack in the -th Erdős–Gallai inequality.
In Lean these objects are IsGraphic, InDprime, norm1', Gf, HasScalingLimit, setF and InteriorF, in the namespace GivenDegreeSeq.Interior.
A function in belongs to the interior of if and only if
Proposition 1.2 turns the hypothesis of the paper's graph-limit theorem into two explicit conditions on . With it, for example, the constant profile with , the degree profile of the Erdős–Rényi graph , is seen to be interior (Remark 3, p. 6). The proposition also describes which limiting degree profiles are robust under small perturbations: away from the boundary given by the continuum Erdős–Gallai inequality and the trivial bounds and .
The Erdős–Gallai criterion is a standard tool for degree sequences, threshold graphs and network models. To the knowledge of this mission it is formalized neither in Mathlib nor on the platform, and a proof of it here is reusable well beyond this paper. The continuum objects , , scaling limits and are shared with the companion mission on the graph-limit theorem (mission 5 of this series). The proposition is proved in the paper; none of it has a machine-checked proof.
The obvious argument passes the Erdős–Gallai inequalities to the limit and back. Going to the limit is routine. Coming back is not, for two reasons. First, the discrete inequalities must hold for every , and near the normalized slack tends to , so positivity of alone gives nothing for . The bounds and of condition (i) are what control this range. Second, the approximating integer sequences must satisfy the parity condition and stay nonincreasing, while still converging in the sense of (2).
For openness, the interior must be taken under , and positivity of near has to be recovered for every nearby from condition (i), not from uniform convergence alone. In the converse direction, perturbations must stay inside , which constrains how may be modified near a zero of .
ℝ → ℝ. Only their values on enter , , , (2) and . Integrals are interval integrals. Every is monotone, hence bounded and integrable on .Fin n, so the paper's is d n ⟨i-1,_⟩ and the paper's is f ((i+1)/n). Degree sequences are vectors in Fin n → ℕ realized by a SimpleGraph (Fin n) and are nonincreasing.Infrastructure needed: the Erdős–Gallai theorem for finite sequences (both directions); Riemann-sum approximation of integrals of monotone functions; an integer-rounding construction with a parity fix. Proofs of the Erdős–Gallai criterion, and of the analytic lemmas on , are welcome independently of the goal.
A backward stochastic differential equation (BSDE) prescribes the terminal value of a process instead of its initial value. Pardoux and Peng (1990) proved that a BSDE with Lipschitz driver has a unique adapted solution. Coupled with a forward diffusion it gives a forward–backward SDE (FBSDE), which represents the solution of a semilinear parabolic PDE (nonlinear Feynman–Kac formula) and, in mathematical finance, the price and hedging strategy of a contingent claim, including path-dependent ones such as lookback and Asian options (El Karoui, Peng and Quenez, 1997). In high dimension or with path-dependent payoffs the PDE route is impractical, so one wants a time-discretization of the FBSDE itself, with a proven rate of convergence.
Zhang (2004) gave such a scheme for terminal values that are Lipschitz functionals of the whole path of the forward diffusion, and proved that it converges in mean square at rate , and at rate for -Lipschitz or Markovian terminal values. The key input is a new -regularity estimate for the martingale integrand . The same regularity estimate underlies the analysis of the Bouchard–Touzi scheme (2004) and of regression-based Monte Carlo methods (Gobet, Lemor and Warin, 2005).
Fix , a probability space carrying a one-dimensional standard Brownian motion , and its natural filtration augmented by the null sets. For the FBSDE is
where , , are deterministic functions and is a deterministic functional of the path .
Assumption 2.3 asks that be continuous, -Hölder in time and Lipschitz in the space variables, that be -Lipschitz,
for càdlàg paths , all with one constant , and that . is -Lipschitz if the supremum can be replaced by .
A partition is , with and ; it is -uniform if for all . The Euler scheme is , , and its step process is on . With the backward scheme is and, for ,
with . The numerical approximations are the step processes and on .
Assume Assumption 2.3 and that is càdlàg. If does not depend on , or is -uniform, then
for , and, if moreover is -Lipschitz or , the same left-hand side is at most (6.6). The constant depends only on , , and . The goal fixes the rates and leaves unspecified.
Theorem 6.1 gives an explicit, implementable scheme for FBSDEs with path-dependent terminal values and a mean-square rate that is sharp up to the logarithm: by Remark 4.3 the factor cannot be removed for -Lipschitz functionals, since it is already present in the uniform error of the Euler step process. Theorem 3.1 is reusable on its own: any time-discretization of a BSDE whose error is measured against needs it.
All results are proved in the paper. As far as is known, none has a machine-checked proof; the platform has no prior BSDE discretization result. The work is formalizing the known proofs, which needs the Itô integral, Itô's isometry and martingale representation, the standard a priori estimates for SDEs and BSDEs, and Doob's maximal inequality in continuous time.
The obvious argument compares the BSDE and the scheme step by step and closes with a discrete Gronwall inequality (Lemma 5.4). Its error terms include , and no pointwise estimate is available: is only square integrable in time, with no continuity modulus in general. The proof therefore needs the summed -regularity of Theorem 3.1, whose proof goes through smooth approximations of the coefficients and of , the representation of by the variational process , and the martingale inequality of Lemma 3.3. The rate comes from the maximum of Gaussian increments, which an estimate of cannot see.
Time is ℝ≥0; the state space is EuclideanSpace ℝ (Fin d); the Brownian motion is the coordinate of a Fin 1-indexed standard Brownian motion; is the augmented filtration. These, the Itô integral and the class are reused from the published modules Peng1990_SMP_Stochastic and ReflectedBSDE_Existence_Setting. Every expectation and time integral of a square is a lower Lebesgue integral in , so a non-integrable error cannot make a bound vacuous; this rules out the trivializing formalization in which a Bochner integral of a non-integrable error is .
The solutions and are quantified as solutions of their equations; the Euler scheme, , , , are constructed. Each constant is chosen before the probability space, the data, the solution and the partition. Disclosed readings: (i) the log-rate statements assume , the paper's " fine enough" (p. 478); (ii) " is càdlàg" includes ; (iii) the uniformity constant of Definition 5.2 is , not , and may depend on it; (iv) the Hölder constant in time is ; (v) , , ; (vi) Lemma 3.3 uses in place of , which strengthens it; (vii) Lemma 5.4 assumes . Completeness of the probability space is not used.
Not formalized here: Lemma 2.2 (smooth approximation of , cited from Ma–Zhang), the background Lemmas 2.4–2.7, and the representation (6.3)–(6.4) of the scheme by functions of the Euler grid values. Welcome contributions: the SDE and BSDE a priori estimates under Lipschitz coefficients, Itô's isometry and martingale representation for the reused Itô integral, and Doob's inequality in continuous time; all are reusable well beyond this mission.
Binary classification asks for a rule that predicts a label from a feature vector , given labelled examples. A classical way to measure how hard this is, due to Mammen and Tsybakov (1999), treats classification as the estimation of a set, the region where label is more likely, and asks how fast the excess misclassification risk of a data-driven classifier can tend to zero. The answer depends on two parameters: the complexity of the class of candidate sets, measured by entropy with bracketing, and the margin parameter , which measures how sharply the conditional probability of label moves away from near the decision boundary.
Tsybakov (2004) showed that empirical risk minimization over a suitable net attains the rate , which approaches ("fast rates") for favourable margins and simple classes, and that this rate is minimax optimal. In practice neither nor is known. The main result of the paper, Theorem 3, constructs a single classifier that adapts to both and attains the optimal rate up to a logarithmic factor simultaneously over a whole family of classes. The margin condition introduced here, often called the Tsybakov margin (or noise) condition, became a standard assumption of statistical learning theory, used for instance in the analysis of support vector machines and of plug-in rules (Audibert and Tsybakov 2007).
Observations are i.i.d. pairs with law . Write for the law of and for the regression function. A classifier is a Borel set , predicting on . The Bayes classifier is , and the excess risk of is
where . Two pseudodistances between sets are used: and its empirical analogue . The empirical risk is .
A class of sets has complexity bound if its -entropy with bracketing for is at most for . The margin assumption (A1) requires whenever , with . A class of distributions is a -class if every has , satisfies (A1), and has complexity bound (Definition 4).
Aggregation. Given classes with complexities and nested approximating sets , let minimize over . With the thresholds
an index is admissible if, for every , some has . The adaptive classifier is with the smallest admissible index.
Under assumptions (A3)–(A4), with a -class for each , , and , fixed, there is such that for all and every ,
Theorem 3 says that a procedure which knows neither the class containing nor the margin parameter loses at most a factor against the optimal rate on every class at once; combined with the lower bound of Theorem 2 it identifies the optimal adaptive rate up to logarithms. Corollary 1 extends it to a continuum of classes . The selection rule is a Lepski-type pairwise comparison of empirical risks, and the analysis is one of the early results on adaptation to the margin.
The result is proved in the paper, with an Appendix that derives the empirical-process inequalities from van de Geer (2000). No part of it is known to have a machine-checked proof. A formalization would produce reusable infrastructure: entropy with bracketing for classes of sets, ratio-type deviation inequalities for empirical processes, and the excess-risk identity for 0–1 loss.
The obvious argument controls each separately and takes a union bound over . That fails: the bound for at a class that does not contain says nothing about , and the adaptive rule compares classifiers from different classes through random thresholds that depend on the empirical distance . The central steps are to show that the true index is admissible with probability uniformly over a polynomially growing number of classes, and to replace by inside the thresholds at a constant-factor cost. Both rest on exponential, ratio-type deviation bounds for suprema over classes of infinite entropy, which are not in Mathlib.
is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, labels are Bool with true ↔ 1, and a distribution is a pair with a probability measure and measurable with values in ; the law of a pair is the published UnderstandingML.condLaw (, then ). Classifiers are sets, risk is measured by via identity (2), and the complexity bound is stated as "some bracketing with exists".
The Section 3 data (, classes, nets, complexities, distribution classes) are indexed by . The formalization commits to the following readings of the page, all disclosed in the items:
Expectations are Lebesgue integrals over the sample, so each one carries the hypothesis that the data-dependent set is jointly measurable in (sample, point). This rules out the trivializing formalization in which a non-measurable classifier has integral and every rate bound holds for free. Probabilities of events involving suprema over uncountable classes are outer measures. Appendix suprema are real suprema over index sets bounded above. The goal is not vacuous: a solution-folder check exhibits a setup satisfying all hypotheses with .
Contributions welcome: bracketing-entropy chaining bounds, the van de Geer inequalities (5.42)–(5.43), and the Appendix lemmas as standalone results.
Automatic verification of programs that manipulate pointers needs procedure specifications: preconditions saying which part of the heap a procedure touches and postconditions saying what it leaves behind. Writing them by hand does not scale to millions of lines of code. Calcagno, Distefano, O'Hearn and Yang (J. ACM 58(6), 2011) infer them compositionally with bi-abduction: when symbolic execution reaches a call whose precondition is not implied by the current state, it asks for the missing memory that would make it hold. This abduction question in separation logic,
is the engine behind the Abductor tool and, later, Facebook Infer.
The question has many solutions ( is always one), so its quality matters. The paper defines an order on solutions that prefers less memory and then logical strength, shows that a best solution always exists as a semantic object, and then asks whether it can be written down and computed in the language that the analysis actually manipulates: symbolic heaps. For the fragment whose only spatial predicate is points-to, it answers yes. That answer, Theorem 3.25, is the goal of this mission.
Values are natural numbers; is nil and the nonzero naturals are the locations. A heap is a finite partial map from locations to values; a stack assigns a value to every variable; a state is a pair . Write when have disjoint domains and is their union. A predicate is an arbitrary set of states. On predicates:
Symbolic heaps of the Points-to Instantiation. Expressions are variables or natural-number constants. A pure formula is a conjunction of and . A spatial formula is a -conjunction of points-to facts , possibly with ; here iff and is the one-cell heap . A symbolic heap is , and a disjunction . In the abduction question (5), , the left-hand side is quantifier-free.
Orders. iff (spatially smaller), and
keeps the states of no proper subheap of which (with the same stack) is in . says that some separate heap satisfies , and the compatible preorder is . Subtraction is .
There is a single algorithm such that for every quantifier-free and symbolic heap of the Points-to Instantiation, the disjunction satisfies
Both halves are part of the goal: the best solution is expressible as a disjunction of symbolic heaps, and it is computable.
The result. Semantically the best solution is (Theorem 3.13 of the paper), a formula that nests and negation around , which no automatic separation-logic prover handles and which says nothing directly about the shape of the missing memory. Theorem 3.25 shows that in the points-to fragment this object collapses to a finite disjunction of symbolic heaps, the format in which an analysis draws "pictures of memory", and that it can be computed. It gives an optimal abduction procedure against which the paper's heuristic procedure can be measured.
Formalizing it. The theorem is proved in the paper, but several steps are given as sketches ("the proof of each of these properties is straightforward", "a straightforward exercise"), Lemma 3.18 has only a proof sketch, and the quantifier-free subtraction display on p. 33 is incomplete as printed (it inspects only the points-to facts and not the pure part of the subtracted heap). A machine-checked development would supply the missing arguments, fix the subtraction step, and give a verified reference implementation of optimal abduction for points-to symbolic heaps. No part of it is known to have been formalized.
The obvious route is to compute directly, but quantifies over all heaps, and symbolic heaps have no syntax for it. The paper splits the problem into three phases (a -minimal solution from a proof system, the incompatible solutions, and ), and each phase carries its own difficulty. The proof system's minimality (Lemma 3.19) must hold against arbitrary semantic predicates, not only symbolic heaps, and it fails as soon as may denote more than one heap for a given stack (the paper notes that adding list segments breaks it). Computing needs subtraction of symbolic heaps with quantifiers, which in turn needs quantifier elimination for Boolean combinations of equalities over an infinite domain, and the paper's quantifier-free subtraction step has to be repaired. Showing that the final disjunction is -least, not merely a solution, needs all three phases.
All statements live in the namespace BiAbduction.Systematic. Values are ℕ with nil 0, locations are the nonzero naturals, variables are ℕ (program and logical variables form one sort), and heaps are maps ℕ → Option ℕ with 0 unallocated and finite domain. Finiteness of heaps is essential, since relies on well-foundedness of the subheap order. Predicates are arbitrary Set (Stack × Heap). The syntax is built from ℕ, Bool, Sum, Prod and List by abbreviations, so "computed by an algorithm" is Mathlib's Computable₂ with the standard Primcodable encodings. The left-hand side has no true conjunct, as in the paper's proofs; the right-hand side may have one. Figure 2 is an inductive relation in which psto may match any right-hand points-to fact. The soundness and -minimality statements assume the paper's bound-variable convention (no variable bound in occurs in ); the goal does not need it.
The goal cannot be met by a degenerate reading. The competitors range over all predicates, not only over disjunctions, and computability refers to fixed standard encodings. The points-to semantics excludes nil addresses, and heaps are finite.
A complete development needs the separation-logic algebra of predicates (associativity and commutativity of , the adjunction between and ), properties of under finite heaps, the soundness and minimality of the proof system, quantifier elimination for equality logic, and a computability argument for list-manipulating procedures. The semantic layer and the quantifier-elimination result are reusable beyond this mission. Contributions to any milestone, and to the supporting lemmas of §3.3 (Lemmas 3.10–3.11, Theorem 3.13), are welcome.
Theorem numbers and page references are those of the accepted manuscript of the J. ACM article (72 pages), not of the typeset journal version.
In a linearly parameterized bandit a decision maker repeatedly chooses an arm from a set and observes a noisy reward whose mean is linear in an unknown vector . The model covers problems in which many arms share a few underlying features: products described by a handful of characteristics, prices, or routes whose costs depend on a few parameters. Because the arms are correlated through , a good policy can learn about every arm from the rewards of any arm, and its regret can be made to depend on the dimension instead of on the number of arms, which may be infinite.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, published in Mathematics of Operations Research, 2010) prove an lower bound on the regret when the arms form the unit sphere, give a matching phase-based policy for strongly convex arm sets, and propose the Uncertainty Ellipsoid (UE) policy for arbitrary compact arm sets. The UE policy is close to the algorithms of Auer (2002) and Dani, Hayes and Kakade (2008), with two differences: it does not need to know the horizon , and it allows and the noise to be unbounded. This mission formalizes its regret bound for general compact arm sets, Theorem 4.1 of the paper.
Fix and a compact set of arms , with the Euclidean norm . Playing arm in period yields
where the noises are independent of each other and of , identically distributed in for each arm, and have mean zero. A policy chooses the arm of period as a function of the history . The regret given and the Bayes risk are
Assumption 1 (p. 13) fixes constants such that, for every : (a) for every arm and every ; (b) every arm has , and contains linearly independent arms with .
The UE policy keeps the ordinary least squares estimate , where , and, with and , the uncertainty radius
It plays in the first periods and then, in each period , an arm maximizing over , with ties broken arbitrarily.
There are constants depending only on such that for every , every compact arm set satisfying Assumption 1, every run of the UE policy, all and all ,
The constants are not fixed: any positive values that work suffice.
The proof in Appendix B proceeds through large deviation inequalities for adaptive least squares (Theorem B.1 for finitely many arms; Lemmas B.3, B.4, B.5 leading to Theorem B.2 for infinitely many), the radius bound (Lemma B.6), the instantaneous regret bound (Lemma B.7), the regret decomposition
(Lemma B.8), and the deterministic Lemmas B.9–B.11, which bound by the value of an optimization problem and that value by .
Theorem 4.1 shows that one policy achieves regret within a factor of the lower bound for every compact arm set, finite or infinite, with sub-Gaussian unbounded noise and without knowledge of . The dependence on the problem is only through and the three constants of Assumption 1; the number of arms does not appear. The large deviation inequalities of Appendix B.1 are also the input of the paper's Theorem 4.2 for finitely many arms.
The result is proved on paper; no machine-checked proof of it is known. A formal development would produce reusable components that are currently absent from Mathlib: a Chernoff-type bound for least squares estimates built from adaptively chosen regressors, the self-normalized inequality of De la Peña, Klass and Lai in the form of Lemma B.3, the determinant recursion behind Lemma B.9, and the law of a bandit history driven by a policy and an arm-dependent noise kernel.
The arms depend on past noise, so with is not a sum of independent terms with fixed weights, and the classical Chernoff bound does not apply. For finitely many arms a union bound over the possible pull counts suffices (Theorem B.1), but its bound grows like and is useless for infinite arm sets. Theorem B.2 instead needs a self-normalized martingale inequality and a covering argument over directions to compare with in the Loewner order. A second difficulty is that the sum of the radii played is not bounded term by term: each term can be as large as , and only the multiplicative recursion of Lemma B.9 shows that large terms are rare.
is EuclideanSpace ℝ (Fin r), so norms are Euclidean. The constants are written ubar, lam0. Policies are deterministic, history-dependent and measurable (measurability is implicit in the paper). The noise is a Markov kernel giving the law of for each arm; the history given is built period by period with fresh independent noise, which is the law of the paper's history. Assumption 1(a) is a bound on a lower Lebesgue integral, so it also asserts finiteness; is . The standing assumptions of Sec. 1.1 (compact , , independent mean-zero noise identically distributed in ) are hypotheses. equals for an infinite arm set. A UE run is any measurable policy that plays first and then a maximizer of after every history that starts with ; on those histories is a genuine inverse.
Deviations from the page, all disclosed in the items: Lemma B.4 is printed for but its proof needs , and at the printed claim fails; it is stated for . Lemmas B.4 and B.5 are printed without "" and are stated for each fixed , the form in which the paper uses them. Lemmas B.9 and B.10 ("with probability one") are stated for every arm sequence that starts with and stays in the ball of radius , which is stronger. Theorem B.1 carries the hypothesis that is finite.
The regret is minus the expected total reward, whose integrand is bounded, so it is never a junk value; the risk bound asserts integrability of the regret in and assumes . The constants are chosen before , the arm set and the instance, so a formalization in which they depend on or on does not prove the goal.
Welcome contributions include proofs of any milestone, in particular the deterministic Lemmas B.9–B.11, and reusable lemmas on matrix determinants, self-normalized bounds and bandit history measures. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF page numbers.