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.
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?
The Riemann mapping theorem says that every simply connected proper domain in the plane is conformally equivalent to the unit disk. For domains with more complicated complements one needs a model with many "holes". Koebe's Kreisnormierungsproblem (1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary components are all round disks or points. Such a model would give a canonical geometric picture of an arbitrary planar domain, and it is closely tied to circle packings, Kleinian groups and the geometry of hyperbolic surfaces of genus zero.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the conjecture in its unrestricted form.
The Riemann sphere is , with local coordinate near finite points and near . A domain is a nonempty connected open subset. A map is conformal at if it is continuous at and, in these coordinates, complex differentiable at with nonzero derivative. A conformal equivalence is a bijection that is conformal at every point of and whose inverse is conformal at every point of .
A closed round disk in is the image of the closed unit disk under a Möbius transformation , ; these are closed Euclidean disks, closed half-planes together with , and complements of open disks. A circle domain is a domain each of whose complementary connected components is a closed round disk or a single point. The complement may be empty, finite, countable or uncountable.
Lean: OAI.Problem047.koebe_circle_domain, open on the platform.
The theorem would complete the existence half of Koebe's problem with no restriction on the number, size or geometry of the complementary components. The paper derives a consequence for hyperbolic geometry (Corollary 8.1): every complete hyperbolic surface of genus zero is isometric to the boundary of the convex hull of a closed set in whose components are round disks or points. Combined with the exhaustion theorem of Ntalampekos and Rajala, it also gives convergent finitely connected approximations for every proper domain. Uniqueness up to Möbius maps is a different question (the He–Schramm rigidity conjecture), addressed in the companion mission on removable boundaries.
The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. Mathlib has neither the Riemann mapping theorem in full generality nor finitely connected circle-domain uniformization, so a formal proof would build substantial reusable complex-analytic infrastructure.
The standard approach uniformizes finitely connected approximations, whose complements are finitely many round disks, and passes to a limit. The difficulty is control at the limit: with possibly uncountably many complementary components, a limiting component can be strictly larger than the round disk obtained by following one approximating disk, or can be a non-round continuum for which no disk was followed at all. Rajala showed that arbitrary exhaustions can indeed fail to produce circle-domain limits, so the approximations must be chosen with care, and all components must be controlled simultaneously, not one at a time.
Sphere := OnePoint ℂ; Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it.IsConformalAt f p: ContinuousAt f p and a nonzero HasDerivAt of in the charts chart p, chart (f p) (identity coordinate at finite points, at ).IsConformalEquivalence f U V: conformal on , MapsTo f U V, and a conformal g on with MapsTo g V U that is a two-sided inverse.IsCircleDomain V: open, IsConnected (hence nonempty), and every connectedComponentIn Vᶜ p is a singleton or IsRoundClosedDisk (a Möbius image of the closed unit disk).U; there is no countability or regularity assumption on the complement.A complete development needs finitely connected uniformization, normal families on the sphere, Dirichlet energy and extremal length, and component correspondence for limits. Contributions formalizing the named intermediate results (Theorem 3.1 finite transfer, Theorem 4.3 compatible barrier lemma, Theorem 5.1 positive-law alternative, Theorem 7.5 retained-test transfer) or the classical He–Schramm countable case are welcome.
A circle domain is a domain in the Riemann sphere whose complementary components are round disks or points. Koebe asked in 1908 whether every domain is conformally equivalent to a circle domain (existence). A second question is rigidity: when is that circle-domain model unique up to Möbius transformations? For finitely and countably connected domains the model is unique, but for domains with uncountably many boundary components uniqueness can fail, and the boundary geometry decides. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable. Rigidity is what makes the circle-domain model canonical, and it connects conformal geometry with removability questions for quasiconformal and Sobolev maps.
The source of this mission, an OpenAI preprint dated September 23, 2026, claims the remaining implication: removability implies rigidity.
The Riemann sphere has local coordinates and . A map is conformal at if it is continuous there and complex differentiable with nonzero derivative in these coordinates; a conformal equivalence is a bijection, conformal on , with conformal inverse. A Möbius transformation is with . A closed round disk is the Möbius image of the closed unit disk. A circle domain is a nonempty connected open set whose complementary components are closed round disks or points.
A compact is conformally removable if every orientation-preserving homeomorphism of that is conformal on is Möbius. A circle domain is conformally rigid if every conformal equivalence from onto another circle domain is the restriction of a Möbius transformation.
Lean: OAI.Problem047.removability_implies_rigidity, open on the platform. The complement may have any cardinality, and no boundary extension of is assumed.
Together with Rajala's counterexample to the converse, the theorem would settle the He–Schramm rigidity conjecture: removability is sufficient but not necessary. It subsumes the earlier sufficient conditions (-finite length, Hölder/John domains, CNED point sets) whenever those boundaries are removable. The intermediate Theorem 5.1, a continuous Sobolev extension theorem across compact totally disconnected conformally removable sets, is of independent interest. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.
Removability is a statement about homeomorphisms of the whole sphere, while rigidity starts from a map defined only on the domain. The obvious route, extending to a homeomorphism of the sphere and then invoking removability, fails: a point component of the complement of may correspond to a disk component of and vice versa, so the coordinates of need not extend continuously, and nothing a priori controls boundary behaviour at uncountably many point components whose union can have positive area.
Sphere := OnePoint ℂ, Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it; conformality uses the charts and with HasDerivAt and a nonzero derivative.IsCircleDomain: open, IsConnected, and every connectedComponentIn of the complement is a singleton or a Möbius image of the closed unit disk.IsConformallyRemovable E: IsCompact E and every homeomorphism h : Sphere ≃ₜ Sphere that is homotopic to the identity (orientation preserving) and conformal on Eᶜ equals some Möbius map everywhere.frontier U; the conclusion is ∃ M, ∀ p ∈ U, f p = M • p.A complete development needs the theory of conformal maps on the sphere, Sobolev functions and Dirichlet energy in the plane, the measurable Riemann mapping theorem (used for the conductivity deformation), and component correspondence. Contributions formalizing Theorem 5.1 (continuous Sobolev extension), Proposition 6.2 (common point traces), or the He–Schramm countable case are welcome.
A bounded symmetric domain is a bounded connected open set in with, at every point, a holomorphic involution having that point as an isolated fixed point. Examples are the ball, the polydisc and the Siegel upper half-spaces in their bounded realizations. They are the universal covers of compact locally symmetric varieties, such as compact quotients of the ball, and play a central role in algebraic geometry and number theory. A classical theme in several complex variables is that a bounded domain with a large automorphism group must be very special: Wong and Rosay showed that an automorphism orbit accumulating at a strongly pseudoconvex boundary point forces the ball, and Frankel showed that convex domains with compact quotients are symmetric.
Kollár and Pardon, studying algebraic varieties whose universal cover is semialgebraic, asked the following bounded-domain question: if a bounded semialgebraic open subset of a complex affine variety admits a properly discontinuous cocompact group of biholomorphisms, must it be a bounded symmetric domain? Semialgebraicity is a finiteness condition on the shape of the domain. It does not make the boundary smooth or convex, and it imposes nothing on the group.
An affine variety is a reduced complex algebraic set , the common zero locus of a set of polynomials. A subset of is semialgebraic if it is a finite Boolean combination of sets and , with a real polynomial in the real and imaginary parts of the coordinates. Let be open in , connected, semialgebraic and bounded. A map on is holomorphic if near each point it is the restriction of a holomorphic map on an open subset of ; a biholomorphism is a homeomorphism that is holomorphic in both directions. A group acts properly discontinuously if the action is proper for the discrete topology on (finite stabilizers are allowed), and the action is cocompact if is compact. is smooth if each point has a neighbourhood in biholomorphic to an open subset of some .
Let be a nonempty connected semialgebraic bounded open subset of a complex affine variety , and let a group act on by biholomorphisms, properly discontinuously and with compact. Then
The goal statement is published on the platform with status Open.
The result itself. The theorem answers the Kollár–Pardon question affirmatively. The ambient variety may be singular and nonnormal, the quotient may have finite quotient singularities, and no convexity, boundary regularity or homogeneity is assumed. It shows that semialgebraicity of a single affine realization forces the classical picture: a compact quotient of a semialgebraic bounded domain is a compact quotient of a bounded symmetric domain. This complements the universal-cover classification of the companion preprint on semialgebraic universal covers of normal projective varieties.
Formalizing it. The statement only uses polynomials, real-analytic Boolean combinations, holomorphic maps on subsets of and group actions, all available in Mathlib. The proof, however, draws on Nash cell decompositions, analytic discs, scaling limits of automorphisms and Vey's theorem on divisible Siegel domains, none of which is formalized. A formal development would provide reusable semialgebraic geometry and several-complex-variables infrastructure.
The classical rigidity arguments (Wong–Rosay, Frankel, Zimmer) need a smooth strongly pseudoconvex or convex boundary point at which rescaled automorphisms converge to a model domain. A semialgebraic boundary can have corners with several complex-normal directions, and the normal fibres can shrink at rates that depend on tangential parameters, so the naive rescaling limit can collapse to a degenerate set. Moreover is not known to be a manifold at the start, so smoothness must be proved from the group action before any differential geometry is available. The heart of the proof is a noncollapse estimate that yields a Siegel-type quadratic model to which Vey's theorem applies.
IsAffineAlgebraic, the zero set of a set of complex polynomials in Fin n → ℂ; is open in the subspace topology of , IsConnected (hence nonempty), bounded, and semialgebraic through an inductive predicate on real polynomials in , closed under complement and union.ProperSMul and a compact orbit space. Each acts holomorphically in the sense of local ambient analytic extension; since also acts, the elements act by biholomorphisms. A non-faithful action is allowed and is harmless, since properness forces finite stabilizers.IsSmooth U asks for local biholomorphisms of neighbourhoods in onto open subsets of some . IsBoundedSymmetricDomain D asks that be open, connected and bounded, and have at each point an involutive biholomorphism fixing it with that point isolated among its fixed points.If a complex manifold is a product , its tangent bundle splits as the sum of the pulled-back tangent bundles of the factors, and each summand is integrable: the bracket of two local holomorphic vector fields tangent to a summand stays in that summand. Conversely, given a holomorphic decomposition , one wants to know whether it comes from a product. Integrability of the summands is the necessary local condition, and it can fail: Höring exhibited a non-integrable summand on the product of an abelian surface with (Höring 2007, Example 2.14). For rationally connected projective manifolds — those in which two general points lie on a rational curve, a class including all Fano manifolds — Höring showed that integrability of one summand already yields a compatible product decomposition, which made automatic integrability the remaining question.
A complex manifold of dimension is a Hausdorff, second-countable space with a holomorphic atlas to . is projective if it admits an injective holomorphic immersion into a complex projective space ; for compact this is a closed embedding.
A rational curve in is a holomorphic map . A compact connected projective manifold is rationally connected if there is a nonempty Zariski-open set such that every pair lies on the image of a rational curve. Here Zariski-open is measured through the projective embedding: is the complement of the common zero set of a family of bihomogeneous polynomials in the two sets of homogeneous coordinates.
A holomorphic splitting is given by a holomorphic field of idempotent linear maps on the tangent spaces, with and , both of positive rank at every point. A family of subspaces is integrable if for every open and every pair of holomorphic vector fields on with values in , the Lie bracket takes values in .
Let be a smooth connected projective complex manifold of dimension at least two which is rationally connected. For every holomorphic decomposition into subbundles of positive rank,
for every open , where denotes holomorphic sections over . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem has no rank or positivity hypothesis, and it settles the smooth rationally connected case of Höring's conjecture. Combined with Höring's product theorem it gives Corollary 1.2: every holomorphic splitting of the tangent bundle of a smooth rationally connected projective manifold comes from an isomorphism identifying with the factor tangent bundles. It also applies to general fibers of the rationally connected quotient of a uniruled compact Kähler manifold, supplying the integrability premise in Höring's structure theorems (Corollary 5.1). Together with the companion preprint on universal-cover splitting for compact Kähler manifolds, it covers both the integrability question and the global product question.
Formalizing it. The statement involves projective embeddings, Zariski-open sets of pairs, rational curves and holomorphic distributions, all expressed from first principles over Mathlib's manifold library. A machine-checked proof would certify a classical-looking but new geometric argument; the compatible product (Corollary 1.2) is not part of this goal.
The bracket of two sections of , projected to , is a tensor , and the task is to show it vanishes. The natural approach is to restrict to rational curves and use positivity, as in the Fano and low-rank cases, but without positivity or rank assumptions the restricted bundles can have summands of either sign and no vanishing follows directly. Smoothness cannot be dropped: a singular rationally connected example with a non-integrable summand exists (Höring 2026, Example 4.3), so the argument must use the manifold structure in an essential way. Rational connectedness is also needed: Höring's example on an abelian surface times is a smooth projective manifold with a non-integrable summand.
ComplexManifold carries its dimension, a Hausdorff second-countable topology, and an analytic (ω) atlas modeled on Fin dim → ℂ. The theorem assumes ConnectedSpace, CompactSpace and 2 ≤ X.dim.ProjectiveEmbedding X is an injective map to ℙ ℂ (Fin (N+1) → ℂ) that is holomorphic and immersive in every affine patch.RationalCurve X is a holomorphic map from given by two holomorphic maps agreeing via ; RationallyConnected e asks for a nonempty, dense, Zariski-open set of pairs (bihomogeneous polynomial complement) all joined by rational curves. Density is automatic for a nonempty Zariski-open subset of the irreducible variety , so stating it does not narrow the class.TangentSplitting X is a holomorphic idempotent field on the tangent bundle with range and kernel of positive rank at every point. Integrable uses VectorField.mlieBracketWithin for sections that are holomorphic on an open set.If a complex manifold is a product , its holomorphic tangent bundle is the direct sum of the tangent bundles of the factors. The converse question asks when a given holomorphic decomposition of the tangent bundle of a compact manifold comes from a product decomposition of its universal cover, with the product realizing the specified summands rather than some other splitting. This is the complex-analytic counterpart of the de Rham decomposition theorem for Riemannian manifolds with parallel complementary distributions (de Rham 1952), but a holomorphic splitting supplies no complete metric making the distributions parallel, so de Rham's argument does not apply. The question sits between foliation theory, Kähler geometry and the classification of projective manifolds with split tangent bundle.
A complex manifold of dimension is a Hausdorff, second-countable space with holomorphic charts to . A Kähler metric is a smooth Riemannian metric on the real tangent bundle that is Hermitian ( for multiplication by ) and whose fundamental form is closed.
A holomorphic splitting of with ranks is given by a field of -linear idempotents , holomorphic in charts, with and ; then , and . A subbundle is integrable if its local holomorphic sections are closed under the Lie bracket. The ordinary universal cover is a connected, simply connected covering space carrying the lifted complex structure.
Let be a compact connected Kähler manifold of complex dimension and a holomorphic splitting into integrable subbundles of positive ranks . Then there are connected, simply connected complex manifolds with and a biholomorphism with
The goal statement is published on the platform with status Open: no machine-checked proof exists yet.
The result itself. The theorem proves the two-summand form of Beauville's conjecture with no flatness, compact-leaf or line-bundle assumption: integrability of both summands and a Kähler metric on a compact manifold suffice. Combined with Höring's integrability theorem it gives compatible product decompositions for every split tangent bundle on a non-uniruled projective manifold (Corollary 1.2), and for projective manifolds with nef and big canonical bundle (Corollary 1.3). With the companion preprint on rationally connected manifolds it also covers split tangent bundles there. The factors may be noncompact, and the conclusion concerns the universal cover, not a finite cover.
Formalizing it. The statement involves universal covers, Kähler forms, holomorphic distributions and biholomorphisms of products, all of which must be expressed with Mathlib's manifold library. A machine-checked proof would certify a global continuation argument (Hartogs-type extension, boundary crossing, path rectangles and monodromy) for which no prior formal treatment exists.
Integrability alone gives, by holomorphic Frobenius, local product coordinates. The obvious strategy is to continue these local products along paths and use simple connectivity of . This fails because a path in one foliation need not be transportable along a path in the other: local product charts can break down, and leaves can be noncompact and dense. Compactness makes every metric complete, but does not make the foliations parallel, so the de Rham argument is unavailable. Beauville's example on ( an abelian surface) shows that even when is a product, a non-integrable complementary summand need not be realized by any product structure, so both integrability hypotheses are needed.
ComplexManifold n bundles a Hausdorff, second-countable type with an atlas modeled on Fin n → ℂ that is smooth for 𝓘(ℂ, Fin n → ℂ), i.e. holomorphic transition maps.KahlerMetric X is a real bilinear form on each tangent space that is symmetric, positive definite, invariant under multiplication by Complex.I, smooth in every chart, and whose fundamental form is closed (the cyclic sum of its chart derivatives vanishes).HolomorphicSplitting X r₁ r₂ is a field of idempotent continuous ℂ-linear maps, holomorphic in charts, with range of rank and kernel of rank . Integrable P says that chart-local holomorphic vector fields with values in the range of have bracket in the range of ; both S.projection and the complementary projection are assumed integrable.OrdinaryUniversalCover X Z is a covering map from a connected, simply connected complex manifold that is a local biholomorphism.CompatibleProduct asks for a homeomorphism , holomorphic with holomorphic inverse, whose differential sends the pullback of onto and the pullback of onto .Zariski's cancellation problem asks whether affine space can be recognized from its cylinder: if a variety satisfies , must ? Algebraically, for a finitely generated commutative -algebra and an independent variable ,
where is a polynomial ring in variables and all isomorphisms are -algebra isomorphisms. The problem is one of the central questions of affine algebraic geometry, closely tied to the recognition of affine space, coordinates of polynomial rings, and polynomial fibrations.
The source of this mission is an OpenAI preprint dated September 23, 2026.
Let be independent variables over and . Put
So is the coordinate ring of the hypersurface . For a -algebra , denotes the polynomial ring in one further variable, and the polynomial ring in variables.
The Lean statement OAI.ComplexCancellation.main is open on the platform.
Theorem 1.1 gives a negative answer to Zariski's cancellation problem over in dimension four, with an explicit counterexample of degree small enough to write in one line. The same polynomial yields two further consequences proved in the paper: is a coordinate of but not of , so the Stable Coordinate Conjecture fails in ambient dimension five (Corollary 1.2); and the maps and are smooth -fibrations that are not Zariski-locally trivial, disproving the Dolgachev–Weisfeiler conjecture over these bases (Corollary 7.1). Cancellation in dimension three over is not addressed.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
The cylinder isomorphism is comparatively explicit: a locally nilpotent derivation sends to , and exponentiating converts into . The hard part is proving . Standard invariants do not help: is smooth, factorial-type obstructions vanish, and topologically is contractible like since its cylinder is . The paper uses additive group actions (locally nilpotent derivations), passing to an associated graded algebra along , lifting actions through a line bundle over a smooth affine quadric, and a rigidity argument based on the Mason–Stothers polynomial abc inequality.
P := MvPolynomial (Fin 5) ℂ with p, s, u, F, J := X 0, …, X 4; x and H are transcribed literally; A := P ⧸ Ideal.span {H}.ringKrullDim A = 4; integrality is IsDomain A; finite generation is Algebra.FiniteType ℂ A.Nonempty (Polynomial A ≃ₐ[ℂ] MvPolynomial (Fin 5) ℂ); the non-polynomiality is ¬ Nonempty (A ≃ₐ[ℂ] MvPolynomial (Fin 4) ℂ). All isomorphisms are -algebra isomorphisms.A complete development needs: explicit polynomial automorphisms (for the cylinder), Krull dimension of hypersurface quotients, locally nilpotent derivations and their kernels, filtrations and associated graded rings, and the Mason–Stothers theorem for polynomials. Contributions formalizing Proposition 2.2, Proposition 3.4 (the graded identification), Propositions 4.1–4.3, Lemma 5.1 (order of a locally nilpotent derivation), Lemma 6.1 (Mason–Stothers) and Proposition 6.3 are welcome.
Seshadri constants measure the local positivity of a line bundle at a point or a configuration of points: how much of an ample class survives after blowing up the points and subtracting equal multiples of the exceptional curves. For points on a surface with ample , a dimension count gives the universal upper bound . Nagata's 1959 conjecture, which came out of his counterexample to Hilbert's fourteenth problem, says that this bound is attained at very general points of the projective plane. On an arbitrary polarized surface, the qualitative Nagata–Biran(–Szemberg) conjecture predicts that the bound is attained at very general points for every sufficiently large . On the symplectic side, the conjecture corresponds to packing stability: large numbers of equal balls fill a four-manifold.
Let be a smooth integral complex projective surface and an ample line bundle, with self-intersection . For a tuple of distinct points, the multipoint Seshadri constant is
the infimum over integral curves through at least one . If is the blow-up at with exceptional curves , then is the largest such that is nef (nonnegative on every integral curve), and always . Let be the set of tuples of distinct points. A property holds at very general tuples if it fails only on a countable union of proper Zariski-closed subsets of .
For every such there is such that for each there is a countable union of proper Zariski-closed subsets of , with , such that for every
The threshold may depend on and is not explicit. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 settles the qualitative Nagata–Biran conjecture for all polarized complex surfaces, with no assumption that is a square or that a plane constant is maximal (the hypotheses needed by Harbourne, Roé and Roé–Ross). Because the conclusion is nefness of the square-zero boundary class, it rules out every curve whose degree-to-multiplicity ratio is below , including curves with unequal multiplicities. Via Eckl's Kähler packing correspondence, it gives the algebraic counterpart of packing stability. The sharp plane case ( in ) is a separate companion result.
Formalizing it. The statement is built from scheme-theoretic foundations: projective surfaces, line bundles, sheaf cohomology, blow-ups by universal property, intersection numbers through Euler characteristics. A complete proof would be among the first machine-checked results about the birational geometry of surfaces. Much of the required infrastructure, such as Riemann–Roch on surfaces, finite-dimensionality of coherent cohomology and the existence of blow-ups, is not yet in Mathlib.
The upper bound is an elementary jet count. Equality requires showing that no curve on the surface has too large multiplicity at the chosen points, for all multiplicity orders simultaneously. Degenerating the points to a special configuration, the usual approach in the plane, fails because the threshold in must be uniform in the jet order: the asymptotic interpolation theorems (Alexander–Hirschowitz) give thresholds depending on a fixed multiplicity bound. Arbitrary surfaces also lack the toric coordinates available on . The source transfers the problem to finite interpolation on an algebraic torus through a nodal divisor in .
Surface: an integral scheme, smooth of relative dimension over , with a closed immersion into some compatible with the structure maps. LineBundle: a locally free sheaf of rank one. IsAmple: the nonvanishing loci of sections of positive powers that are affine form a neighbourhood basis.Ext^n(𝒪, M) in the category of sheaves of modules, and dimensions are finrank ℂ. Then and , by Riemann–Roch. If cohomology were infinite-dimensional, finrank would return ; finite-dimensionality for projective schemes is part of what a solver must prove.IsClosed, ≠ univ, with a point outside all of them).sInf over integral curves with positive total multiplicity.PointBlowup, characterized by its universal property, and the exceptional ideal sheaves . The inequality is for every integral curve on the blow-up.Let be the -th prime and the -th gap. By the prime number theorem the average gap near is about . A great deal is known about how large individual gaps can be, but much less about how often large gaps occur. A natural question is whether, for each fixed , a positive proportion of all gaps exceed . Erdős and Prachar (1962) asked a closely related question about the sequence : do the indices where it increases have positive lower density?
The source of this mission is an OpenAI preprint dated September 25, 2026.
For every fixed real there are and with
and
The Lean statement OAI.Problem344.large_gaps_and_ratio_density is the conjunction of these two claims and is open on the platform.
Theorem 1.1 says that gaps of size are not rare for any fixed : they occupy a positive proportion of the indices up to every large . This is a statement about the frequency of large gaps, not about the size of the largest one, and it does not follow from the Erdős–Rankin or Ford–Green–Konyagin–Maynard–Tao constructions. Corollary 1.2 answers the Erdős–Prachar question: since is equivalent to , it follows from Theorem 1.1 with . The constants are not made explicit.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
Counting gaps differs from counting empty intervals: a single very long gap contains many starting points of prime-free intervals, so a positive proportion of empty intervals can come from a sparse set of gaps. Results of the latter kind (Bazzanella–Languasco–Zaccagnini, Tao's empty-interval argument) therefore do not give gap counts. The proof needs a sieve weight that makes a prime in likely while making almost surely prime-free, and then a multiplicity argument (the last prime before the empty interval is selected by at most values of ) to convert weighted interval mass into a count of distinct gaps. Making the second interval nearly empty requires an alternating family of divisor-sum squares whose adjacent dimensions nearly cancel.
prime n = Nat.nth Nat.Prime (n - 1), so prime 1 = 2; largeGapIndices C N filters Finset.Icc 1 N by C * log (prime n) < prime (n+1) - prime n in ℝ.lowerAsymptoticDensity A = sSup {d | ∃ N0, ∀ N ≥ N0, d ≤ initialCount A N / N}, which equals the liminf because the ratios lie in .ratioIncreaseIndices = {n | 1 ≤ n ∧ prime n / n < prime (n+1) / (n+1)} in ℝ.A complete development needs the prime number theorem, the Bombieri–Vinogradov theorem, smooth Goldston–Yıldırım/Maynard divisor-sum correlations, and averages of the Hardy–Littlewood singular series. These are widely reusable. Contributions formalizing Proposition 2.1 (weights for adjacent intervals), Proposition 3.1 (moment identities and a detector bound), Proposition 4.2 (cancellation between high dimensions), Proposition 5.1 (uniform mixed moments) and Lemma 5.4 (singular series in boxes) are welcome.
An Egyptian-fraction expansion writes a positive rational number as a sum of distinct unit fractions . Every fraction with has one, by the greedy algorithm, but greedy expansions can be long. The basic quantitative question is how many terms are needed in the worst case for a fixed denominator . Let be the least length of an expansion of with denominators , and . Erdős proved in 1950 that , showed that (already for ), and conjectured that the double-logarithmic order is correct. The question appears in Erdős–Graham's 1980 problem book and as Erdős Problem 304. The same circle of questions asks how many expansions of with exactly terms exist, and which integers can appear as denominators in them (Erdős Problem 293).
For integers , an expansion of is a finite list of integers with
The fraction need not be in lowest terms and the denominators are unbounded. is the least such , and
For , is the number of tuples with ; is the set of integers occurring as some in such a tuple; and .
Every with has an expansion, and there are absolute constants and such that for every
No values of the constants are fixed. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 answers Erdős's 1950 conjecture (Erdős Problem 304) affirmatively. The lower bound is classical; the content is the uniform upper bound for every numerator. As consequences, the paper determines the double-logarithmic order of the number of representations of (Corollary 1.2) and of the least integer absent from all -term expansions of (Corollary 1.3), improving van Doorn–Tang's lower bound to a double exponential.
Formalizing it. All statements are elementary, with no analytic objects beyond logarithms, so a formal proof would give a complete machine-checked account of a problem from Erdős's list. The proof uses residue distribution of divisors, uniform divisor moments and a probabilistic construction, none of which is machine-checked. The elementary pieces — finiteness of , the denominator bound , and the padding lemma — are independently checkable and useful for other unit-fraction problems.
The greedy algorithm and divisor methods (Erdős; Tenenbaum–Yokota) lose a factor because they treat each numerator individually. The proof instead builds an auxiliary denominator for which almost every numerator in a large range has a short expansion, and descends through ranges. The obstacle is that the exceptional numerators at each level could accumulate during the descent; controlling them requires a uniform moment bound for small divisors in shifted intervals. For Corollary 1.3, an additional difficulty is that the exact term must survive every operation that lengthens the expansion.
OAI.ShortEgyptian: expansions are List ℕ that are strictly increasing (Pairwise (· < ·)), with entries and rational sum ; minLength a b is an sInf and maxMinLength b the maximum over . The existence conjunct guarantees that sInf is taken over a nonempty set, so the bounds cannot hold through a junk value.Problem337 milestones use Fin k → ℕ tuples (StrictMono, entries for and for expansions of ); is Set.ncard, and is sInf of the missing denominators. Finiteness of and of the expansion sets, which make these values meaningful, are separate statements in the proposal. In Corollary 1.3 the slopes are real liminf/limsup, accompanied by the explicit eventual bounds.Real.log; all constants are existential, apart from the explicit , and of the source.Euler's totient counts the integers in coprime to . Many integers share a totient, and most integers are not totients at all, so counting the distinct values of is much harder than counting integers with a given factorization. Let
The size of was studied by Pillai, Erdős, Hall, Pomerance, Maier and Ford over most of the twentieth century; Ford's 1998 estimate determines up to a bounded multiplicative factor but leaves open whether has an asymptotic equivalent, and Erdős and Hall's question whether .
This mission asks for a formal proof of the explicit asymptotic formula and the Erdős–Hall regular-variation property, as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Logarithms are natural and is the -fold iterate. For let , let be the unique root of , and set
For large put , , the phase , and ; the factor is Ford's counting scale.
For each the preprint defines an explicit arithmetic coefficient , , from a finite set of "tail witnesses" (tuples of primes , , and a cofactor , subject to explicit size and recurrence constraints, ) by inclusion–exclusion over witnesses with a common totient , weighted by (formula (2.8), p. 5). Here is the least preimage, and when the limit exists. The coefficient is defined without reference to .
for .
uniformly on , with , and
For let and . Then converges uniformly and ; if some totient has then and , and otherwise and . The positive alternative holds for .
The result itself. The formula replaces Ford's bounded uncertainty by an explicit function of the phase , built from finite arithmetic data, and answers the Erdős–Hall question: is regularly varying of index . Theorem 2.2 answers, in weighted form, Erdős's question on how least preimages are distributed in intervals , reducing it to the existence of a "seed" totient with . Whether such seeds exist for every (equivalently, whether is unbounded) is not settled by the preprint.
Formalizing it. This is analytic number theory at full strength: Ford's structure theorems for totient preimages, sieve bounds for two or three linear forms in shifted primes, simplex volume computations and an inclusion–exclusion limit. Mathlib has the totient and the prime number theorem in some forms but not these sieve and distribution results. The definitions in this mission (the renewal root , the witnesses, ) are explicit and can be checked independently of any proof.
Counting integers with a typical factorization is a volume computation, but counts values, and different can have the same totient. The preprint must show that, outside a negligible set, distinct long prime prefixes give distinct values (Proposition 5.1, p. 22, and Proposition 5.3, p. 27), which needs a uniform comparison estimate for products of shifted primes (Proposition 4.2, p. 17), while short discrete tails that may collide are kept exactly and handled by inclusion–exclusion (Lemma 6.4, p. 30). The limits are taken in a specific order ( with fixed, then ), and no continuity of is available, so all errors must be uniform in the phase.
IsTotient v means for some ; V x counts totients in ; ell v is Nat.find of the least preimage (junk value for non-totients, never used on them).rho is the sInf of roots in of ; the root is unique, so this is the source's .AH H f s is formula (2.8) with finsum over totients and over nonempty finite sets of witnesses with ; the witness set is finite for each , so the finsums are genuine finite sums. A f s is limUnder atTop; the goal asserts uniform convergence, so the junk value is never used.mainTerm x = x / log x * G x (m x) * A 1 (theta x); asymptotic equivalence is Tendsto (V x / mainTerm x) atTop (𝓝 1).coefficient_nonnegative is stated for every , while the source states it for sufficiently large ; for small the witness set is empty or the inclusion–exclusion is still a probability, so this is a harmless strengthening.companion_zero_case restates alternative (ii) of Theorem 2.2 in a separate definition file (TotientCompanionZero) with identical definitions.For a positive integer , Jacobsthal's function is the least such that every run of consecutive integers contains an integer coprime to . Equivalently, is the longest interval that can be covered by choosing one residue class modulo each prime divisor of (the classes shifted by the interval's start). Its maximum over integers with at most prime divisors,
governs how long a stretch can be sieved out by primes. It is linked to gaps between consecutive primes (long covered intervals produce large prime gaps, as in the Erdős–Rankin and Ford–Green–Konyagin–Maynard–Tao constructions) and to the limits of the linear sieve. Jacobsthal asked, and Erdős recorded, whether .
The source of this mission is an OpenAI preprint dated September 25, 2026.
Both are stated in Lean as the existence, for each , of a length satisfying IsJacobsthalBound k m with the displayed size bound. The goal OAI.Erdos970.Erdos970Final.erdos_970_iterated_log is open on the platform.
Theorem 1.1 answers Jacobsthal's question affirmatively, uniformly over all prime sets and interval positions, and removes the logarithmic losses in the bounds of Vaughan and Iwaniec, going slightly below the quadratic scale. It shows that the linear sieve can be pushed to its limiting parameter , where the lower sieve function vanishes, by retaining a boundary contribution. The gap to the best lower bound (roughly ) remains large; Vaughan suggested .
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The constant is not made explicit.
The linear sieve gives a lower bound for the number of uncovered integers only when the sieving range is below the square root of the interval length, which is exactly where the exponent 2 comes from; at the critical parameter the main term of the lower-bound sieve vanishes, so the standard argument yields nothing and a loss appears. One must keep the boundary term that the leading linear-sieve calculation discards, and then show that the actual prescribed residue classes do not deviate much from a reference calculation. Positivity of the reference calculation alone does not suffice: the comparison requires an inverse estimate for a witnessing edge of a decreasing-prime tree, variance bounds, and stopping-time counts for hard endpoints.
IsJacobsthalBound k m: for every n : ℕ with 0 < n and n.primeFactors.card ≤ k, and every a : ℤ, some i < m has (a + i).natAbs.Coprime n.JacobsthalQuadratic: ∃ C > 0, ∀ k > 0, ∃ m, IsJacobsthalBound k m ∧ m ≤ C k^2.JacobsthalIteratedLog: the same with bound C k^2 / (log (log (3k)))^2; for the denominator is positive.IsJacobsthalBound identically.A complete development needs the fundamental lemma of the sieve, Buchstab-type functions of the linear sieve, prime number theorem estimates in short ranges and progressions, the additive large sieve, a lattice-point count on plane curves, and renewal-type arguments for a continuous path process. Contributions formalizing Theorem 1.2 (the quantitative covering estimate), Lemma 2.1 (fundamental lemma of the sieve), Proposition 6.3 (positive reference margin), Proposition 8.2 (inverse estimate for an edge) and Corollary 9.3 are welcome.
An integer is -power-free if no prime power divides it (zero is never -power-free). For a fixed integer polynomial one expects to be -power-free for a positive proportion of integers , given by an Euler product of local densities, as soon as no prime th power divides every value of . The heuristic is a sieve: discard the with for each prime . Small primes are handled by the Chinese remainder theorem; the problem lies with primes larger than the range of , where can be divisible by only if it has an unusually large square-full part. The case , where , is the first exponent left open by classical methods. Its best-known instance is the squarefreeness of , singled out by Erdős in 1953 and again in his 1965 survey.
Let be irreducible over , of degree , and let . Define
The local admissibility condition is for every prime : no prime th power divides all values of . The predicted density is
Let be irreducible over with , put , and assume for every prime . Then the Euler product converges,
For this is the paper's new Theorem 1.1; for it follows from Browning's theorem. Already the case (squarefree values of quartics such as and ) is new. The goal statement is published on the platform with status Open.
The result itself. The theorem closes the exponent for every degree, answering Erdős's question about and giving the first unconditional squarefree-density theorem for an arbitrary admissible irreducible quartic. No primitivity or sign condition on is required. The same large-prime estimate also gives densities for separable products and simultaneous power-freeness of several polynomials (Corollary 1.3).
Formalizing it. The statement is elementary, but its proof uses number-field factorization, the unit theorem, determinant methods for counting points on surfaces and curves, and explicit Hilbert-function computations. None of these components is machine-checked. A formal proof would certify a result that the literature had only reached conditionally (on ) or in higher degrees. The finite-prime sieve and the deduction of the density from a large-prime tail bound are reusable for other power-free-value problems.
The sieve over primes is routine. The obstacle is the primes : one must show that very few have for some such (Proposition 1.4, with a power saving ). Counting solutions of as integer points on the surface with determinant methods succeeds only when is large; in the intermediate range the point counts are too weak, and the existing determinant bounds stop exactly at .
Polynomial ℤ whose image in Polynomial ℚ is irreducible, with natDegree ≥ 4; the exponent is f.natDegree - 2 (at least , so the natural-number subtraction is harmless).PowerFree k a says no prime has , so is not power-free, matching the source convention; negative values are allowed.tprod over Nat.Primes; the goal asserts Multipliable explicitly, so the constant is not a junk value, together with and .Goldbach-type problems ask which sets are sumsets of primes. The inverse Goldbach problem, due to Ostmann (1956), reverses the question: can the set of primes itself, up to finitely many changes, be written as a sumset with both and having at least two elements? Ostmann conjectured that it cannot: the primes are asymptotically additively indecomposable. The problem is a clean test of how much additive structure the primes can carry, and it connects sieve theory (the primes avoid one residue class modulo each prime) with inverse questions for the large sieve.
The source of this mission is an OpenAI preprint dated September 24, 2026.
Let and let be the set of positive primes. For the sumset is . Two sets are asymptotically equal if their symmetric difference is finite. A decomposition is nontrivial if and ; the trivial decompositions are excluded.
Theorem 2.3 is the core of the proof; Lemma 2.2 reduces Theorem 1.1 to it by a short sieve argument.
The goal OAI.Ostmann.inverseGoldbach is open on the platform.
Theorem 1.1 resolves Ostmann's conjecture. The conclusion controls both requirements of an eventual decomposition: if and contains every sufficiently large prime, then contains infinitely many composite numbers. The proof does not go through the general inverse large-sieve conjecture of Green and Harper; it uses the simultaneous residue restrictions together with coverage of every large prime directly.
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The statement is elementary, so the formal target is short; the difficulty is entirely in the proof.
Counting alone cannot work: sieve bounds put and near , which is compatible with the lower bound forced by covering the primes. The known necessary conditions (large intersections with quadratic images) fall short of the near-containment that Green and Harper's conditional route requires. The proof must turn the local information (modulo each prime , the images of and are disjoint) into a global contradiction: it rules out correlations with translated multiplicative characters of every order, compares a positive sumset statistic with its average over the primes, and handles residue indicators with no prescribed algebraic form via a finite-field comparison of binary trees. The paper runs to about 80 pages.
primes = {n : ℕ | Nat.Prime n}; sumset A B is Mathlib's pointwise A + B on Set ℕ.A.Nontrivial means has two distinct elements.InverseGoldbach asserts Set.Infinite (sumset A B ∆ primes); TwoInfiniteSummandsImpossible uses EventuallyPrimeSumset A B := ∃ N, ∀ n ≥ N, n ∈ A + B ↔ n.Prime, which is equivalent to a finite symmetric difference.OAI.Ostmann.main is the same statement as the goal without the definition file and is included as a reference item.A complete development needs the additive large sieve (Montgomery–Vaughan), Gallagher's larger sieve, Mertens-type estimates, character sums over finite fields including the quadratic large sieve, prime number theorems in progressions with the exceptional character, and Fourier analysis on . Contributions formalizing Lemma 2.1 (fixed shifts), Lemma 2.2 (finite summands), Lemma 2.4 (square-root bounds), Proposition 3.1, Corollary 4.2 (mixed-character decorrelation), Proposition 5.1 and Lemma 6.1 (tree comparison) are welcome.
Let be the largest prime factor of an integer . The classical theory of smooth numbers (Dickman 1930, Ramaswami 1949, de Bruijn 1951) shows that has a limiting distribution: the proportion of with tends to , where is the Dickman function. Multiplicative structure of and of is expected to be independent, since consecutive integers share no prime factor, but proving independence of such "additive shifts" of multiplicative data is the core difficulty of the Chowla/Elliott circle of problems. Erdős and Pomerance (1978) asked whether and are asymptotically independent with Dickman marginals, and, as a consequence, whether holds for exactly half of all (a comparison question usually attributed to Erdős and Turán).
For , is the largest prime dividing . The Dickman function is the continuous function with
equivalently for . For a property of integers and real , the natural density at scale is
For every fixed ,
with running over all reals and ordinary, unweighted counting. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.1 says that, in natural density, and are independent with Dickman marginals. It settles the Erdős–Pomerance independence question positively, removes the logarithmic weighting of Teräväinen's theorem and the exceptional scales of Tao–Teräväinen, and implies the Erdős–Turán comparison: because the limiting marginal is continuous, the product law gives no mass to the diagonal, so each strict ordering has density (Corollary 1.2). Previous unconditional work only gave lower natural densities, never the existence of the density.
Formalizing it. The goal is a clean density statement about elementary objects, but its proof combines Matomäki–Radziwiłł short-interval estimates, sieve bounds, a divisor amplifier, graph comparison and cut-norm sampling. No part of this argument is machine-checked. Even the one-variable Dickman law (the marginal case) is not in Mathlib, and would be a reusable milestone in its own right.
Independence of and is a binary correlation problem for multiplicative data, of the same nature as the two-point Chowla conjecture. Tao's entropy-decrement and logarithmic-averaging method handles such correlations only with weight , or at almost all scales; the step that fails for ordinary density is ruling out a positive correlation along a sparse sequence of scales. The indicator is also not multiplicative, so short-interval theorems for multiplicative functions do not apply to it directly.
Nat.maxPrimeFac n (largest element of the prime factor list, a faithful backport of the Mathlib definition) represents ; its junk values at are irrelevant since counting starts at .realDensity P X is #{n ∈ [2, ⌊X⌋] : P n} / X as a real number, and limits are Tendsto … atTop over real , matching "the limit over all real ".(n:ℝ)^a, and the hypotheses , are explicit.stepApprox and evaluating the -th iterate at ; this agrees with the Dickman function on , which is the only range used (). A wrong would make the goal false, so this definition is part of what solvers should check.A mathematical program with complementarity constraints (MPCC, also called MPEC, mathematical program with equilibrium constraints) is a nonlinear optimization problem in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such constraints model equilibria inside an optimization problem: bilevel programs whose lower level is replaced by its optimality conditions, Stackelberg games, traffic and electricity market equilibria, contact problems in mechanics. See Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996), doi:10.1017/CBO9780511983658.
The complementarity constraints make the standard theory fail. At every feasible point the Mangasarian–Fromovitz constraint qualification is violated, so the Karush–Kuhn–Tucker conditions are not necessary for optimality, and standard NLP solvers lose their convergence guarantees. A common remedy is relaxation: replace the MPEC by a family of ordinary nonlinear programs depending on a parameter , solve them for , and study the limits of their stationary points.
The first relaxation scheme, and the reference point for all later ones, is due to Scholtes (Convergence properties of a regularization scheme for mathematical programs with complementarity constraints, SIAM J. Optim. 11 (2001), doi:10.1137/S1052623499361233). Scholtes showed that limits of stationary points of the relaxed programs are C-stationary when MPEC-LICQ holds at the limit. Hoheisel, Kanzow and Schwartz (Preprint 299, University of Würzburg, 2010; later Math. Program. 137 (2013), doi:10.1007/s10107-011-0488-5) compare five relaxation schemes and weaken the constraint qualification in each convergence theorem. For Scholtes' scheme, their Theorem 3.1 replaces MPEC-LICQ by the weaker MPEC-MFCQ. This mission formalizes that theorem.
The MPEC (1) is
with continuously differentiable and feasible set . For a point the paper uses the index sets , , and .
A standard nonlinear program has constraints , . Its point satisfies the Mangasarian–Fromovitz constraint qualification (MFCQ) if the gradients are linearly independent and some direction has for all active and for all . A stationary point is the -part of a KKT point: is feasible and there are , with and .
The tightened program TNLP keeps , and imposes on , on , and on . MPEC-MFCQ holds at if MFCQ holds at for TNLP.
A feasible is weakly stationary if there are multipliers , , with
, , on and on . It is C-stationary if such multipliers can be chosen with, in addition, for all .
Scholtes' relaxed program replaces by and keeps all other constraints of (1). The notation means a sequence of positive parameters decreasing to .
Let , let be a stationary point of , and let with MPEC-MFCQ at . Then
No feasibility of is assumed; it is part of the conclusion.
Theorem 3.1 says that Scholtes' scheme, run to the limit, produces C-stationary points under a constraint qualification strictly weaker than the one in Scholtes' original result. MPEC-MFCQ is the natural assumption here: under it the KKT multipliers of the relaxed programs need not converge, and the theorem shows that a convergent subsequence of suitably modified multipliers still exists. The result is the first of a family of convergence theorems in the paper (the schemes of Lin–Fukushima, Kadrani–Dussault–Benchakroun and Steffensen–Ulbrich follow the same pattern) and the baseline against which those schemes are compared.
The theorem is proved in the paper; it is not open. To the extent a search of the Prove2Me catalog shows, no MPEC stationarity concept, MPEC constraint qualification or relaxation result has been formalized there, and Mathlib has no theory of constraint qualifications for nonlinear programs. The mission produces a machine-checked proof of Theorem 3.1 and, along the way, reusable statements of Definition 2.1, MFCQ, KKT points and the MFCQ/positive-linear-independence equivalence for general nonlinear programs.
The obvious argument takes a limit of the KKT multipliers of . That fails twice. First, under MPEC-MFCQ the multiplier sequence need not be bounded, so there may be nothing to take a limit of; boundedness has to be recovered from MPEC-MFCQ through positive-linear independence, a theorem of the alternative. Second, the multiplier of the product constraint multiplies , which is not a multiplier of or alone; how it is redistributed depends on whether lies in , or , and the sign condition on comes from the support disjointness between and the multipliers of , , which uses . Compactness, index-set bookkeeping along a subsequence and continuity of all gradients have to be combined.
EuclideanSpace ℝ (Fin n), gradients are Mathlib's gradient, and is the inner product. Constraint indices are Fin m, Fin p, Fin l (0-based); may be .P.IsC1 (ContDiff ℝ 1 for each function) of the goal and of milestones 4 and 5. Milestones 1–3 are pointwise linear algebra and assume no smoothness.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 .In the local model of differential privacy, no trusted curator holds the data: each individual randomizes their own record before handing it to the analyst. This is the model of randomized response in survey statistics and of the privacy-preserving telemetry deployed by large software vendors. 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), asked which learning tasks remain possible in this model. Their answer (§5) is that local algorithms are exactly as powerful as statistical query (SQ) algorithms in the sense of Kearns (J. ACM 1998), up to polynomial factors. This mission formalizes one direction of that equivalence: every local algorithm run on i.i.d. data can be simulated by an SQ algorithm.
This is the fourth of five missions on the paper. Mission III formalizes the converse direction (Theorem 5.7). All theorem numbers refer to arXiv:0803.0924v3.
A database is . Here its entries are drawn i.i.d. from a probability distribution on .
There is an absolute constant such that for every -local algorithm making queries there is an SQ algorithm with the following properties against every distribution and every valid oracle:
The constant is the paper's . The tolerance is the proof's own choice.
The result. Lemma 5.8, combined with Theorem 5.7, shows that a concept class is learnable by a locally private algorithm if and only if it is learnable with statistical queries (Theorem 5.14). Every SQ lower bound therefore becomes a lower bound for local privacy. For instance, parity functions are privately learnable by a centralized algorithm (Theorem 4.4) but not by a local one, because parities need exponentially many statistical queries (Corollary 5.15, which also uses the SQ lower bound of Blum et al., STOC 1994).
Formalizing it. The result is proved on paper. As far as we know it has no machine-checked proof. The paper's proof is a few paragraphs and leaves the model implicit: what an SQ algorithm with a random number of queries is, how an adversarial oracle interacts with it, and in what sense the per-randomizer errors add up over adaptively chosen randomizers. The formal statement makes each of these explicit. The milestones isolate the estimates the proof uses, so they can be proved independently of the composition argument.
The estimates in the milestones are elementary inequalities. The difficulty is in the goal. First, the oracle's answers, and therefore the estimates , change from iteration to iteration, so the simulated distribution is not a fixed rejection sampler: the output law must be controlled iteration by iteration against an adversary. Second, the SQ algorithm has no bound on its number of steps. Its output law is a limit over an unbounded run, and its query count is an expectation that is finite only because every iteration terminates with probability bounded away from zero. Third, in the interactive case the randomizers applied to one entry are correlated through the entry. The simulation must sample from the conditional law given earlier answers on that entry, while the errors of all steps combine along adaptively chosen histories.
R u : PMF W. The simulation uses the point probabilities . Every map is required to be measurable.Reusable beyond this mission: the SQ-algorithm state machine with expected query count, the statistical difference of sub-probability mass functions, and the model of interactive local algorithms. Welcome contributions include proofs of the estimate milestones, a general lemma bounding the statistical difference of sequentially composed approximate samplers, and the termination and expected-runtime analysis of rejection sampling with varying acceptance probabilities.
Large service systems such as call centers and hospital wards are modelled as many-server queues: identical servers, customers arriving according to a general process, service requirements drawn independently from a general distribution , and a single first-come-first-served queue. When is not exponential the number of customers in system is not Markov, and a tractable state must keep track of how long each customer in service has been served. Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011)) take as state the number in system together with the age measure, the point measure of the ages of the customers in service, and prove a functional law of large numbers: scaled by , these processes converge to the unique solution of a deterministic system, the fluid equations. Earlier fluid and diffusion analyses of the queue worked with other state descriptors (Reed, Ann. Appl. Probab. 19 (2009); Whitt, Oper. Res. 54 (2006)); the measure-valued description records the elapsed service time of every customer in service, which is the information a non-exponential service distribution requires.
This mission covers the deterministic half of that result: the fluid equations are well posed, and their solution is given in closed form.
Service requirements have a density that vanishes on , , and the mean is normalized to one, . Let and let be the hazard rate on ; is locally integrable on but not integrable on it. For a measure and a function write , and for the constant one.
The data are a triple in
where is the cumulative arrival process, the initial number in system and the initial age measure (per server, so the total capacity is one). A càdlàg pair , with a sub-probability measure on in the weak topology, solves the fluid equations if for every : (3.4); for every test function
(3.6); and the nonidling condition (3.7). Here is the cumulative departure process and the cumulative entry into service. Equation (3.5) is a weak form of a transport equation: mass moves to the right at unit speed, is killed at rate , and enters at age at rate .
For every :
Uniqueness of the fluid solution is what turns tightness of the scaled -server processes into convergence: every subsequential limit solves the fluid equations, so all coincide (the paper's Theorem 3.7). The representation (3.11) reduces the measure-valued equation to the scalar process , and the continuity estimate of Theorem 4.6 says the fluid solution is a Lipschitz function of the arrival process. Both are used in the paper's study of long-time behaviour, where converges to the measure with density , and (3.12) is the form of the entry rate used there.
The results are proved in the paper. None of them, and no part of the measure-valued fluid model, has a machine-checked proof. Formalizing them produces a checked weak-solution theory for a transport equation with an unbounded killing rate and a measure-valued boundary input, which is a reusable piece of infrastructure for other age- and residual-time-based queueing models.
The central step is Theorem 4.1. The naive approach treats (4.2) as a first-order PDE and integrates along characteristics, but the solution is only a càdlàg path of measures, is merely locally integrable and blows up near , and may jump, so classical characteristics are not available; the test functions must not vanish on the boundary , since that is where the entry term lives. The second difficulty is in Theorem 4.6: the entry process is defined implicitly through the nonidling condition, and comparing two solutions requires a first-crossing argument that distinguishes whether the system is below, at or above capacity at that time.
The service law is its density (ServiceLaw), with below , and mean one. Time is read on ; every condition is stated for . Measures of the fluid model are FiniteMeasure ℝ carried by , whose topology is weak convergence, so càdlàg paths are càdlàg in with the weak topology. The paths of Theorem 4.1 and Lemma 4.5 are ℝ → Measure ℝ with values Radon on (possibly infinite) and càdlàg in the vague topology. is an extended number. The integral in (3.4) is a lower integral in , and , are its real value. is the Lebesgue–Stieltjes measure of , with no atom at . A function of bounded variation is a difference of nondecreasing càdlàg functions vanishing at .
Explicit choices: compact support of test functions is relative to , so need not vanish (with supports taken in the entry term of (3.5) would vanish identically); and equal to the datum are clauses of the fluid equations, but not of the age equation, where is arbitrary; functions in , and are represented by functions on of the same class, of which only values on are read; norms in Lemma 4.5 are computed in , since may be infinite. Two printed statements are corrected: in Theorem 3.5 the paper's right-hand side of the equivalence lists (3.6) and (3.11); the nonidling condition (3.7), part of the fluid equations on the left, is kept on the right, as the proof requires. In (4.10), is replaced by , which is what Lemma 4.5 and (4.9) give.
A fluid solution is defined by the weak transport equation (3.5), never by the representation (3.11) or by a formula for in terms of ; with such a definition the equivalence of the goal would be an unfolding of definitions.
A complete development needs Lebesgue–Stieltjes integration by parts for càdlàg functions of bounded variation, the Riesz description of the vague topology, and uniqueness for weak solutions of transport equations; these are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 3.5 separately, are welcome. The paper's Section 4.3 machinery (the abstract and simplified age equations, Lemmas 4.12–4.13, Propositions 4.15–4.16) is not posed here and may be formalized as supporting lemmas.
A backward stochastic differential equation (BSDE) prescribes the value of a process at a terminal time and asks for an adapted process that reaches it while following a given drift. In mathematical finance the price of a contingent claim, and its hedging strategy, solve such an equation; when the market has frictions (different borrowing and lending rates, for example) the drift, called the driver, is nonlinear and no closed form exists. Numerical methods for BSDEs are therefore methods for pricing and hedging under nonlinear models, and also for semilinear parabolic PDEs, which BSDEs represent probabilistically.
Gobet, Lemor and Warin (Ann. Appl. Probab. 15 (2005), arXiv:math/0508491) proposed and analysed a simulation scheme in which every conditional expectation of a backward time-stepping recursion is replaced by a least-squares regression on finitely many functions, as in the Longstaff–Schwartz method for American options. Their analysis splits the total error into three parts: time discretization (Theorem 1, from Zhang's results), replacing conditional expectations by projections on function bases (Theorem 2), and replacing those projections by empirical regressions on simulated paths (Theorem 3). This mission formalizes the second part.
Timeline. Zhang (Ann. Appl. Probab. 14 (2004)) and Bouchard and Touzi (Stoch. Proc. Appl. 111 (2004)) established the rate of the time discretization. Bouchard and Touzi's regression error (their reference [6] in the paper, Theorem 4.1 there) was expressed through the residuals of the scheme's own iterates. Gobet, Lemor and Warin (2005) gave the bound in terms of the residuals of the discrete BSDE, together with estimates on .
Fix a horizon , dimensions , a drift and a diffusion matrix , both Lipschitz in ((H1)), and a driver with
For put and . On a probability space with a filtration , the increments are -measurable, independent of and Gaussian ; is the -th component. The Euler scheme is , . An -adapted process extends by extra state variables, and the terminal value is , square integrable.
Write . The discrete BSDE is and, for ,
A function basis () is square integrable with invertible Gram matrix . is the orthogonal projection of onto the span of the basis, and .
The projection–Picard scheme with iterations (Definition 1) produces and , starting from , where minimizes
Finally .
For small enough,
Theorem 2 shows that the projection errors of a backward regression scheme only add up over the time steps, with a constant that does not grow with , and that they are measured by the residuals of the discrete BSDE itself. That makes the influence of the basis directly computable (the paper's §6 does so for Voronoi-cell indicators), and shows that Picard iterations already give an error of the order of the time discretization. Combined with Theorem 3 it gives the complete error budget of the algorithm.
The result is proved in the paper; to our knowledge none of it is machine-checked. A complete development provides a formal -regression calculus for discrete BSDEs (projections on random bases, conditional expectations against Gaussian increments, contraction of Picard maps in ) and a backward discrete Gronwall lemma, all reusable for other regression schemes. One printed step, (14), fails at (see below), so a formal proof also certifies that the theorem survives the repair.
The obvious argument compares the scheme with the discrete BSDE one step at a time and applies Gronwall. It fails for : carries a factor , and a naive bound summed over steps explodes. A usable bound has to account for the conditional variance of given , not only its second moment. The second difficulty is that the projection does not commute with the driver: projection errors enter at every step through the nonlinear , and must be bounded by residuals of and , not of the scheme's iterates. A third is the Picard step: at the iterate is computed with , so it is not an iterate of the contraction of milestone 3, and the printed inequality (14) fails there; an extra term in is needed.
The Lean development lives in the namespace RegMCBSDE.Projection. Points are in EuclideanSpace ℝ (Fin d), the matrix norm in (H1) is the Frobenius norm, and all expectations of squares are lower Lebesgue integrals in , so no junk value of a Bochner integral can make an inequality vacuous. Component (from ) of is the paper's , and the bases are indexed by Fin (q+1) with for .
Committed readings:
Contributions welcome: proofs of the milestones, and the Mathlib-level lemmas they need (conditional expectation of a product with an independent centered Gaussian, moments of the Euler scheme, the projection identity for -measurable bases).
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.
Robust dynamic programming replaces the single transition law of a Markov decision process by a set of laws, and values a policy by its worst-case expected reward over that set. Iyengar (Robust dynamic programming, CORC Tech Report TR-2002-07, 2004; Math. Oper. Res. 30(2), 2005) and Nilim and El Ghaoui (Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5), 2005) showed that under a rectangularity assumption the robust value satisfies a robust Bellman equation. Each step of that equation solves, for every state–action pair, an inner problem
the worst-case expectation of a value vector over the ambiguity set . Robust value iteration is only as practical as this inner problem is cheap.
The ambiguity sets of interest come from statistics: when transition probabilities are estimated from data, natural sets are confidence regions around the empirical distribution. Section 4 of Iyengar's report studies three such families: relative-entropy balls (Lemma 4), a χ² approximation of them (Lemma 5), and an outer approximation (Lemma 6). This mission formalizes the χ² case. The relative-entropy case is already posed on the platform as RobustMDP.EntropyInner.kl_ball_inner_problem_dual (Nilim–El Ghaoui series), up to the sign change .
Let be a finite set of states and let be the probability measures on . For and write
Fix a centre with for every (in the paper is the empirical next-state distribution of one state–action pair) and a radius . The χ² set (46) is
Since , the relative entropy is at most the χ² distance, so lies inside the relative-entropy ball of radius : it is a conservative approximation of it. The Lean development names these objects expect, variance, chiSqDist, chiSqSet, relEntropy and the dual objective dualObj q t v μ , all in the namespace RobustDP.ChiSquare.
For every value vector ,
where ranges over vectors with componentwise. Both extrema are attained. The lemma's complexity claim, for (48), is a statement about an algorithm and is not part of the mission.
Two further results stand on the same definitions: the inequality of Section 4.2, and the analogue of Lemma 5 established in the proof of Lemma 6 (p. 20):
The result. Lemma 5 reduces a worst-case expectation over a curved convex set of probability vectors to a concave problem in one scalar, which the paper solves by sorting. This makes robust value iteration with χ² ambiguity sets about as expensive as nominal value iteration, up to a logarithmic factor. The identity also explains the shape of the answer: a mean minus a standard-deviation penalty, applied to a value vector truncated from above at the level . The truncation comes from the constraint .
Formalizing it. The result is proved in the paper; no machine-checked proof is known. A complete formalization gives a verified finite-dimensional duality theorem for a quadratic constraint combined with polyhedral constraints, which is the computational core of χ²-ambiguity robust MDPs and of χ²-divergence distributionally robust optimization in general. Lemma 6's printed formula (57) is false (see below); the mission poses the corrected identity that the paper's proof establishes.
The obvious argument drops the constraint . Without it, the minimum of the linear function over the ellipsoid follows from Cauchy–Schwarz and equals . The page notes (p. 19) that earlier work solved only this relaxed problem. With the minimizer of the relaxation can leave the simplex, so the problem has an ellipsoidal constraint, a polyhedral constraint and an equality at once. The multiplier of is what Lemma 5 has to handle. Equality of the primal minimum with the dual supremum needs a duality theorem that is not in Mathlib in this form. Attainment of the dual maximum over the unbounded cone needs an additional argument, namely that an optimal multiplier has the truncation form (53).
Fintype; vectors are functions S → ℝ; is Mathlib's stdSimplex ℝ S. Nonemptiness of follows from . Finiteness is the standing restriction of Section 4 (p. 15).IsLeast and IsGreatest of image sets, so the goal asserts attainment on both sides, as the page's "minimize" and "max" do.0 ≤ μ). The multiplier of the equality ranges over . The page's "" in (50) is a misprint: the proof of Lemma 6 writes , and the optimal may be negative.⨆ over an unbounded set, would make the statement junk.Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, signal detection and factor models all start from the eigenvalues of computed from samples of an -dimensional vector. When is comparable to , the eigenvalues of no longer approximate those of the population covariance . The question is then whether a few large population eigenvalues ("spikes") are visible in the sample spectrum at all, and how the top sample eigenvalue fluctuates when they are.
Baik, Ben Arous and Péché (Ann. Probab. 33 (2005) 1643–1697) answered this for complex Gaussian samples. They found a sharp threshold , where , now called the BBP phase transition. This mission formalizes the supercritical half of the answer, Theorem 1.1(b).
Timeline.
Let , , , be independent standard complex Gaussians: with independent real normal variables of mean and variance . Fix a unitary matrix and positive population eigenvalues . The samples are
which are independent mean-zero complex Gaussian vectors with covariance . The sample covariance matrix is , and is its largest eigenvalue.
The regime has with and in a compact subset of . A fixed number of the differ from . For some the top coincide, , with common value in a compact subset of . The others, , lie in a compact subset of .
The limit law is the finite GUE distribution. Let . Then
which is the law of the largest eigenvalue of a Gaussian unitary ensemble matrix (Definition 1.2).
The milestones follow the proof in §4, in attack order:
Here are the orthonormal polynomials for the weight and their leading coefficients.
The result. Below the threshold the top eigenvalue sticks to the bulk edge . Above it, Theorem 1.1(b) and Corollary 1.1(b) show that separates from the bulk to the explicit location . Its fluctuations shrink from order to order , and their law is the top eigenvalue of a GUE, with the multiplicity of the spike. This gives:
Formalizing it. The result is proved in the paper and is not open. Nothing in this mission has a machine-checked proof yet. A complete development would include:
The two contour lemmas (4.1, 4.2) and the Hermite identities are elementary and are footholds. Proposition 4.1 and Lemma 1.1 are substantial. The paper does not prove Lemma 1.1 but cites it as a standard result of random matrix theory (its references [28, 41]).
The obvious route is to diagonalise the sample matrix, write down the eigenvalue density and take a limit. That density involves the Harish-Chandra–Itzykson–Zuber integral. Its large- limit is not accessible directly, because the spike enters through a determinant with nearly coincident columns.
The paper instead starts from an exact Fredholm-determinant formula (Proposition 2.1, posed in mission 1 of this series). In it the kernel factors into two contour integrals and with phase . Above the threshold the two factors are governed by different points. has a nondegenerate saddle at . For the natural saddle lies beyond the pole at , so the contour must be deformed through a pole of order , and the leading term is a residue rather than a saddle contribution. The estimates must hold uniformly in and in the remaining spikes, and the convergence must be strong enough (Hilbert–Schmidt) to pass to Fredholm determinants.
Model. Complex Gaussian samples with mean zero and no centring. , with the factor . for every unitary . This is the model of the paper's (59), (61) and Proposition 2.1; the introduction's mentions of , of centring and of the real density (1) are inconsistent with those formulas. is the supremum of the eigenvalues of the Hermitian matrix , and probabilities are measures of sets of sample arrays.
Regime. The regime is in sequence form:
The fixed margins encode the compact subsets whose open ends move with . Convergence is pointwise in .
Analytic conventions.
Ruled-out trivialisations. Five shortcuts would make the statements trivial, and none is available:
Infrastructure. The needed infrastructure is the complex Wishart model, eigenvalues of random Hermitian matrices, Fredholm determinants of integral operators, and contour integrals with uniform estimates. The Hermite and Fredholm layers can be reused for any orthogonal-polynomial ensemble. Contributions welcome:
The secretary problem asks how well an online decision maker can do when items arrive one at a time in random order and each must be accepted or rejected on the spot. With a single selection, the classical rule (observe a fraction, then take the first item better than everything seen) selects the best item with probability about , and no rule does better. Many allocation problems are not single-choice: a seller with identical goods facing bidders who arrive over time, an advertiser with a budget of impressions, an employer with openings. Each asks the multiple-choice secretary problem: how much of the best achievable total can an online rule collect when selections are allowed?
Kleinberg's 2005 SODA paper answered this for the sum objective. It gave a recursive algorithm whose expected total is at least times the sum of the largest values, so the ratio tends to as grows, and stated a matching upper bound for every algorithm, whose proof the extended abstract omits. The motivating application was online auctions: the algorithm becomes a strategyproof mechanism for selling identical items to bidders who arrive and depart over time, extending the single-item online auction of Hajiaghayi, Kleinberg and Parkes (EC 2004).
Timeline. Dynkin (1963) and the classical literature settle with ratio . Hajiaghayi, Kleinberg and Parkes (2004) turn the single-item rule into an online auction. Kleinberg (2005) proves for selections, with the explicit constant . Babaioff, Immorlica, Kempe and Kleinberg (2008) survey the resulting family of generalized secretary problems and their use in online auctions.
Let be a finite set of distinct non-negative real numbers. The elements of are revealed in a uniformly random order: each of the orders has probability . After each arrival the algorithm decides, irrevocably and using only the values seen so far, whether to select it. At most elements may be selected. Write for the set of the largest elements of (all of if ) and
for their sum, the best total any rule could collect knowing in advance.
Kleinberg's algorithm is defined by recursion on :
The expected value of the algorithm is taken over the random order and over every binomial draw at every level of the recursion.
The statement is uniform in and ; it says nothing beyond the explicit constant printed in the paper.
The paper proves the theorem by induction on . Its sketch introduces , the set of the first arrivals, , the modified value of a set (the sum of its elements lying in ), and , the number of elements of exceeding . The milestones are its stated claims, in order:
The result. Theorem 2.1 shows that random arrival order costs only a factor when many items are sold, against the constant for a single item. With the paper's matching upper bound, it pins down the optimal rate for the -choice problem. It is the base of the paper's strategyproof online auction for identical goods and a standard reference point for the later literature on secretary problems with combinatorial constraints and on online allocation in the random-order model.
Formalizing it. The paper is a two-page extended abstract, and the theorem's proof is a sketch: several steps are described as "easy", a stochastic-domination argument is stated without detail, and the behaviour of the algorithm when fewer than elements have been observed is not specified. A machine-checked proof would supply the complete argument for the explicit constant. The result is proved on paper only in this sketch; no machine-checked proof of it is known.
The obvious argument fixes and treats the threshold as if it split the remaining elements exactly. Both steps fail. With a fixed , the first arrivals are not a uniform subset of and is hypergeometric, so the clean binomial computations of the sketch are not available; the binomial choice of is what makes uniform. And the number of later elements beyond fluctuates by order : the second phase may run out of budget before reaching all of , or accept elements outside . Controlling this fluctuation, while the cap of also counts the first phase's selections, is the central step. The induction must then combine a recursive guarantee on a random, random-sized prefix with this estimate.
The Lean development fixes these conventions.
Finset ℝ with all elements non-negative; distinctness is automatic. The arrival at time (0-based) under the order is the -th smallest element of , and expectations over the order use the published uniform average SecretaryWD.DiscUpper.uniformAvg.PMF over sets of selected positions, defined by well-founded recursion on . The base case is the published SecretaryWD.DiscUpper.classicalSecretary. is Mathlib's PMF.binomial (1/2). At the algorithm selects nothing, for totality only; all statements assume .A complete development needs: the uniform-subset law of a binomially sized random prefix; conditional expectations over random subsets; tail and absolute-deviation bounds for sums of geometric variables and a stochastic-domination argument; and a careful treatment of the recursion through PMF.bind. The first and third are reusable beyond this mission, for other random-order and sample-based algorithms. Proofs of any milestone, of auxiliary lemmas about the random prefix, and of the goal by a route different from the sketch are all welcome.
Random growth models and random matrices share limit laws. The first exact instance was found by Johansson (Shape fluctuations and random matrices, Comm. Math. Phys. 2000), who showed that the last passage time of a lattice model with geometric or exponential weights has the law of the largest eigenvalue of a Laguerre (complex Wishart) random matrix. Baik, Ben Arous and Péché (Ann. Probab. 33 (2005)) extended the identity to weights whose rate depends on the row. On the matrix side this is a sample covariance matrix with a general population covariance ; on the growth side it is a corner growth model, or a series of exponential queues, with inhomogeneous service rates.
The identity is the reason the paper's main result, the phase transition of the largest sample eigenvalue as a few population eigenvalues ("spikes") cross the critical value , is also a theorem about last passage percolation and tandem queues. In the queueing reading, a spike is a slow server, and the phase transition describes how slow a few servers must be before they change the centring and the fluctuation scale of the exit time.
Timeline:
Last passage time. Attach a real weight to every site of the grid . An up/right path from to is a sequence of sites starting at , ending at , each step adding or . The last passage time is
Exponential environment. Given positive numbers , the are independent and is exponential of mean , i.e. density on . All sites of row share one rate.
Sample covariance matrix. Let , , , be independent standard complex Gaussians (real and imaginary parts independent ). For a unitary and (308), the samples are mean-zero complex Gaussian vectors with covariance , and
Schur functions and geometric weights. For a partition , the Schur function is the sum over semistandard Young tableaux of shape of . A geometric variable of parameter has .
For , positive and every unitary ,
The two sides are defined independently: one by a maximum over lattice paths of exponential weights, the other by the spectrum of a Gaussian random matrix.
The proposition makes every distributional statement about in the paper a statement about last passage percolation with row-dependent rates: the (generalised Tracy–Widom) fluctuations at the critical spike value, the Gaussian fluctuations above it, and the fixed-dimension limit. Through (312)–(313) it also covers the exit time of customers from exponential servers in series, an operations research object. The geometric formula (310) is the entry point of the RSK method for exactly solvable growth models.
These results are proved in the literature; the paper cites (310) and (311) and derives (307) from them by a limit. None of them is machine-checked as far as this series knows. Formalizing them requires a Lean development of Schur functions, the Cauchy identity and the RSK correspondence on matrices with nonnegative integer entries, and of the Wishart eigenvalue density, each reusable well beyond this mission.
The recurrence (313) is elementary. Everything else is not. The geometric formula (310) needs the RSK bijection between nonnegative integer matrices and pairs of semistandard tableaux of the same shape, together with Schensted's theorem that the first row of the shape is the last passage time; neither is in Mathlib. The passage from (310) to (307) is a scaling limit , , , in which a sum over partitions must converge to a multiple integral. The matrix side needs the joint eigenvalue density of a complex Wishart matrix with general , which uses the Harish-Chandra–Itzykson–Zuber integral. A direct coupling of the two sides is not known; the identity is an equality of laws, proved by computing both.
The development lives in the namespace SpikedWishart.LastPassage. Conventions:
expMeasure with rate .A formalization in which either side of (309) is defined through the other, or through (307), would be trivial and is excluded: both laws are defined from scratch. Contributions are welcome on RSK and Schur function infrastructure, on the Wishart density, and on the measurability of .