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?
Place a convex body in the position coordinates and its polar in the momentum coordinates of the standard symplectic space . The resulting Lagrangian product links two problems. Its volume is the Mahler volume product , and its symplectic capacities measure how large a round ball can be squeezed into it by a symplectic map. Since symplectic maps preserve volume, a ball of capacity inside forces . Artstein-Avidan, Karasev and Ostrover showed that the Hofer–Zehnder capacity of equals for every origin-symmetric and connected Viterbo's volume–capacity conjecture to Mahler's conjecture (Duke 2014). Whether actual balls of capacity close to fit, i.e. whether the Gromov width also equals , was open.
This mission asks for a formal proof that it does, as claimed in an OpenAI preprint dated September 22, 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.
An origin-symmetric convex body is compact, convex, has nonempty interior, and satisfies . Its polar is . On put , and let
A symplectic embedding of an open set into is a map on that is a topological embedding, maps into , and whose derivative preserves at every point. The Gromov width is the supremum of capacities for which embeds symplectically into .
For every and origin-symmetric convex body , .
For every and every origin-symmetric convex body ,
and for every there is a symplectic embedding . No embedding at capacity exactly is asserted.
The result itself. It answers the symmetric-polar-product width question with no smoothness, strict convexity or unconditionality assumptions, and through volume preservation it implies the symmetric Mahler inequality in every dimension (Corollary 5.3). For it also transports finite ball packings satisfying strict volume and pairwise-capacity conditions into (Corollary 5.5, p. 17). It is specific to symmetric polar products: the general Viterbo conjecture is false.
Formalizing it. Mathlib has smooth manifolds and differential forms but no symplectic capacities, nonsqueezing, or Moser's deformation method. A formal proof would need these, together with a conformal map of the disk with explicit boundary estimates. These components are reusable across symplectic geometry. No machine-checked computation of a Gromov width of a non-trivial domain is known.
The upper bound follows from Gromov nonsqueezing and a supporting-cylinder argument (or from the Hofer–Zehnder computation). The lower bound is the hard direction: knowing does not produce any ball, and explicit embeddings were previously known only for special families ( balls, the cube). The preprint's route (Sections 2–4) needs balls of capacity close to from holomorphic maps vanishing to order , and a momentum scale that is uniform up to the tips of a conformal lens, where slice heights approach as grows; a non-uniform estimate does not suffice.
EuclideanSpace ℝ (Fin n); phase space is their product. polar uses the real inner product; polarProduct K is interior K ×ˢ interior (polar K).capacityBall n c is the open ball , so a ball of radius has capacity .HasSymplecticEmbedding U V: some e with ContDiffOn ℝ ∞ e U, IsEmbedding on the subtype U, MapsTo e U V, and for all .gromovWidth is an sSup in ℝ≥0∞ of the admissible capacities, so an unbounded set would give ⊤; the goal asserts the value 4 and separately every capacity below .Welcome contributions: a Lean notion of symplectic embedding between open subsets of , Gromov nonsqueezing (as an axiom-free target in its own right), and volume preservation for symplectic maps.
The volume product of a convex body measures how large a body and its polar can simultaneously be. For a body without a distinguished centre, the polar is taken about the point that makes it smallest, the Santaló point, so the product is invariant under all invertible affine maps. The Blaschke–Santaló inequality identifies ellipsoids as the maximizers. Mahler's conjecture for general convex bodies asks for the minimizers and predicts simplices, with minimum value . The question arose from Mahler's work on polarity and the geometry of numbers, and it is the sharp form of the Bourgain–Milman reverse Santaló inequality.
This mission asks for a formal proof of the general Mahler conjecture with its equality case, as stated in an OpenAI preprint dated September 22, 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.
A convex body is a compact convex set with nonempty interior; is Lebesgue measure and the Euclidean inner product. For an interior point , the polar of about is
and the volume product is
The infimum is attained at the unique Santaló point . A simplex is the convex hull of affinely independent points.
For every and every convex body ,
with equality if and only if is a simplex.
The result itself. It is the exact form of a problem open since the 1930s and previously settled only in dimensions and and for polytopes with few vertices. Because the infimum over centres is taken, it gives the same lower bound for at every interior point . Via the known geometric-to-functional implication, the preprint derives the sharp functional Mahler inequality for log-concave functions and an entropy–transport inequality (Corollary 1.2, p. 4; Corollary 8.1, p. 41). The symmetric conjecture, with the larger constant , is a different statement treated in a companion preprint.
Formalizing it. The proof combines convex cones and their Laplace transforms, Gaussian Sobolev calculus, Moreau's decomposition, matrix divided differences, and certified one-variable inequalities. A formal proof would provide checked versions of these tools and of the Santaló point's existence and uniqueness. No machine-checked proof of the conjecture in any dimension is known.
Symmetrization does not apply, the volume product is not convex along natural deformations except in restricted families (shadow systems), and local minimality at simplices says nothing about distant bodies. In the preprint's route the main obstacle (Introduction, pp. 2–3) is that the Jacobian matrices of the Gaussian-averaged cone projections neither commute nor increase in : bounding them separately loses both the sharp constant and the equality case. Controlling them jointly requires comparing the whole family with spectral thresholds of a linear Gaussian matrix (Sections 5–7), and equality must then force the cone to split into half-lines.
EuclideanSpace ℝ (Fin n) with IsCompact, Convex ℝ and nonempty interior, and .polarAt K z is the polar about ; volumeProduct K is the sInf over interior K of (volume K).toReal * (volume (polarAt K z)).toReal. For an interior the polar is bounded, so toReal reads the true volume; the index set is nonempty because the interior is.volumeProduct K = (n+1)^(n+1)/(n!)^2 iff K = convexHull ℝ (range v) for some affinely independent v : Fin (n+1) → _.Welcome contributions: polar bodies and their volumes in Mathlib, the Santaló point, Laplace transforms of convex cones, and Gaussian integration by parts.
The Hardy–Littlewood maximal function replaces a function by the largest of its averages around each point. It is the basic tool for differentiation theorems and singular integrals, and it is bounded on for but not on . Kinnunen showed that it also preserves first-order Sobolev regularity: it is bounded on for , because pointwise (Kinnunen 1997). At this argument breaks, since is unbounded on . Hajłasz and Onninen asked whether the gradient estimate nevertheless holds (Question 1 in Ann. Acad. Sci. Fenn. Math. 2004). The question is a test of whether maximal operators improve or destroy regularity at the endpoint, where the usual machinery is unavailable.
This mission asks for a formal proof of the planar centered-disk case, as stated in an OpenAI preprint dated September 26, 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.
Identify with the Euclidean plane and write for the open disk of radius centered at . For a locally integrable real function , the centered disk maximal function is
The space consists of integrable whose distributional gradient is represented by an integrable vector field , i.e. for all . Norms of gradients are Euclidean: . For the signed estimate, put and .
There is an absolute constant such that for every real and with a power of two (including ),
with independent of , and the number of dyadic scales.
There is an absolute constant such that for every real , is finite almost everywhere, locally integrable, belongs to , and has a globally integrable weak gradient with
The result itself. It resolves the planar centered-disk case of the Hajłasz–Onninen question with no radiality or support assumption. As a consequence (Corollary 6.3, p. 39) the bound extends to inputs and yields a co-area type perimeter bound for level sets of . The constant is absolute but not optimized. Higher dimensions, other centered maximal operators, and continuity of in remain separate questions.
Formalizing it. Mathlib has Lebesgue integration, weak derivatives only in limited form, and no maximal-function regularity theory. A formal proof would need distributional gradients, Poincaré inequalities on squares, dyadic multiscale decompositions and a vector-measure representation of bounded distributional derivatives (the preprint's Appendix A). These pieces are reusable across harmonic analysis.
For one bounds and uses the strong maximal inequality, which fails for . One-dimensional proofs order the optimizing intervals, and that ordering has no analogue for families of centered disks. Fractional-order proofs use that optimizing balls overlap little, a mechanism that degenerates at order zero. The preprint (Sections 2–5) instead proves the signed finite-band estimate uniformly in the number of scales: it uses a vanishing first moment at interior maximizing radii, a concentration-in-a-thin-shell lemma (Lemma 2.4, p. 8), and two multiscale constructions that pay for direction changes in scale and space. A variation bound alone would leave a possibly singular derivative measure; removing the singular part needs the signed form of Proposition 1.2 applied to locally mean-subtracted inputs (Section 6).
EuclideanSpace ℝ (Fin 2). maximal f x is an ℝ≥0∞-valued supremum over all real of lower Lebesgue integrals of over Metric.ball x r divided by ; the goal asserts it is finite a.e. before passing to maximalReal = toReal.HasWeakGradient f g is the integration-by-parts identity against every compactly supported test function, coordinatewise; the input is Integrable f, Integrable g, HasWeakGradient f g, which is exactly with weak gradient g. The bound is stated against this g, so it does not depend on a choice of representative.InW11Loc asks for local integrability and a locally integrable weak gradient; the goal also asks for one integrable weak gradient G with ∫ ‖G‖ ≤ C * ∫ ‖g‖, C ≥ 0 chosen before f.sSup over the closed radius band ; the band envelope is continuous in , so the supremum is finite. Inputs are ContDiff ℝ ∞ with compact support.The Hilbert transform is the basic singular integral of harmonic analysis. In the plane one can take it along a line through each point, with the direction of the line allowed to depend on the point: given a unit vector field , integrate along the segment through in direction . Whether such directional Hilbert transforms are bounded on is one of the central problems connecting singular integrals, Kakeya-type geometry and time–frequency analysis. If depends on only one coordinate, the problem already contains Carleson's theorem on almost-everywhere convergence of Fourier series. For general fields some regularity of is necessary, and some truncation of the integration length is necessary because a field can turn.
Stein asked whether a Lipschitz field suffices when the integration length is at most a small multiple of . In the formulation of Lacey and Li, this is a uniform weak- conjecture. A parallel conjecture of Zygmund concerns the corresponding maximal averages.
The source of this mission, an OpenAI preprint dated September 25, 2026, claims the uniform strong bound at short scale for every Lipschitz field.
Let be Lipschitz with . For the short directional Hilbert transform is
The direction is frozen at the output point . For a Schwartz function the principal value exists at every point, since .
There are absolute constants and such that every unit field with satisfies, for all ,
and the truncations and the principal value extend to bounded operators on with norm at most . The constants and are existential; no numerical value is fixed. The Lean statement OAI.LipschitzHilbert.main is open on the platform.
The proposal also contains OAI.LipschitzHilbert.uniform_truncation, the rescaled form for -Lipschitz fields at every outer length . By the dilation it is the same estimate at the reciprocal-Lipschitz scale; its explicit constant is a convention of the formalization, not of the paper.
The theorem answers the short-scale form of Stein's question affirmatively and with a strong (not only weak-type) bound, for fields depending on both coordinates and with no regularity beyond Lipschitz. Earlier unconditional results required the field to depend on one variable, to be constant along a foliation, to be analytic, to take lacunary directions, or restricted the frequency to one annulus. The uniformity in the inner truncation is an operator bound for each truncation, which is what the principal value and the weak-type bound are derived from.
The result is claimed in an OpenAI preprint of 87 pages; it has not been peer reviewed and no machine-checked proof exists. The Lean goal records the complete short-scale conclusion; a formal proof would certify a long chain of time–frequency arguments (wave-packet decompositions, size and density selection, a Lipschitz Kakeya input, and a phase-gain iteration).
Restricting to short scales limits how far the field turns but does not make the operator a Fourier multiplier: the line of integration still varies with the output point. Positive (maximal) operator bounds lose all oscillation, while the one-variable reduction to Carleson's theorem is unavailable when depends on both coordinates. The known band-to-full reassembly reduces matters to one vertical frequency band, but on a band one needs a restricted estimate with a logarithmic gain in the ratio of the measures of the input and test sets; the Lacey–Li Kakeya estimate only provides a polynomial loss in that ratio, so an additional oscillatory saving is required.
EuclideanSpace ℝ (Fin 2); inputs are SchwartzMap Plane ℂ, norms are eLpNorm _ 2 volume in ℝ≥0∞.v : Plane → Plane with LipschitzWith 1 v and ‖v x‖ = 1 for all x.twoSidedTruncation v ε a f x is the sum of interval integrals over and of ; smoothPrincipalValue integrates the symmetric quotient over , with the removable value at filled by the derivative.ShortHilbertConclusion a C bundles the five clauses (truncation bound for , principal-value bound, weak-(2,2) bound at every finite nonzero level, and bounded Lp extensions agreeing a.e. on Schwartz inputs). The goal asks for and .A complete development needs singular-integral and Littlewood–Paley machinery on , wave-packet analysis and a Lipschitz Kakeya maximal estimate; much of this is reusable for other time–frequency problems. Contributions formalizing the band-restricted estimate, the band-to-full reassembly, or the one-dimensional inputs (the maximal truncated Hilbert transform) are welcome.
The triangular Hilbert transform is a bilinear singular integral on the plane that couples translations in two different coordinate directions:
Paired with a third function, it becomes a trilinear form whose three inputs depend on the three pairs of variables of . This "triangular" or entangled structure defeats the time–frequency methods that handle the one-dimensional bilinear Hilbert transform. Boundedness of this operator is a model problem for multilinear singular integrals with simplex structure, and is closely tied to norm convergence and variation of ergodic averages for two commuting transformations. Thiele listed the symmetric case () as Problem 13 in the 2017 collection Some problems in harmonic analysis.
For complex functions on and , the hard truncation is
and the maximal truncation is
For the finite truncations converge absolutely outside a common null set, and is measurable (Lemma 7.1 of the source).
There is an absolute constant such that, for all complex ,
The Lean goal also includes the measure-theoretic preliminaries of Lemma 7.1: almost every point is a point where all finite truncations converge absolutely, and is almost-everywhere measurable. The goal statement is published on the platform with status Open.
The result itself. A uniform bound for the maximal operator controls a truncation chosen independently at each point, which is stronger than a uniform bound on each . It yields existence of the joint principal value almost everywhere and in (Theorem 7.2). By duality and a determinant-one change of variables, it gives endpoint-uniform bounds for the symmetric trilinear triangular form , which resolves Thiele's Problem 13 positively. Earlier bounds all grew with the number of scales.
Formalizing it. The estimate is a clean statement in Mathlib's and lower-integral language. Its proof combines matrix trace inequalities, Gaussian heat-flow energies and discretization limits, all of which would have to be built. The finite-dimensional matrix inequalities (Sections 2–3 of the source) are self-contained and reusable for other entangled multilinear forms.
Time–frequency analysis, which handles the one-dimensional bilinear Hilbert transform, does not adapt to the triangular form because its three inputs are entangled: each depends on a different pair of variables, so no single frequency-localization serves all three. Energy and telescoping methods (Kovač; Durcik) work for bipartite forms, but the triangular cycle is the documented obstruction. Previous cancellation estimates lose a factor depending on the number of scales . The maximal version adds a further difficulty: the truncation endpoints vary from point to point, so the energy argument must tolerate entries that switch on and off at independently chosen scales, without losses depending on the number of scales or on matrix dimensions.
ℝ × ℝ → ℂ with Lebesgue measure; hypotheses are MemLp F 3 and MemLp G 3 (which include a.e. strong measurability).truncation F G E z is the Bochner integral of over , with endpoints packaged as Endpoints ().GoodPoint requires integrability on the annuli for all , hence on every finite annulus. maximal is the ℝ≥0∞-valued supremum over all endpoint pairs at good points, and elsewhere. The goal asserts that almost every point is good, so this junk value cannot help.ℝ≥0∞, compared with eLpNorm F 3 * eLpNorm G 3. The constant is an existential ℝ≥0, so it is finite and independent of .For a set the distance set is . Falconer (1985) asked how large a set must be, measured by Hausdorff dimension, to force to have positive length. Examples built from lattices show that dimension is not enough in general, and Falconer conjectured that any compact set of dimension strictly greater than suffices. The question is the continuous analogue of Erdős's distinct-distances problem and has been a driving problem for geometric measure theory and Fourier restriction theory: progress on it has repeatedly come from, and fed back into, spherical averages, restriction estimates, decoupling and radial projections.
The source of this mission is an OpenAI preprint dated September 23, 2026.
The goal OAI.Falconer.falconer_distance_conjecture is open on the platform.
Theorem 1.1 resolves Falconer's distance conjecture in every dimension, with no regularity assumption beyond the strict dimension bound: no equality of Hausdorff and packing dimension, no Ahlfors regularity, no product structure. The threshold is sharp by Falconer's lattice examples, and no endpoint assertion is made. The result is unpinned: it does not assert that a single point has at the threshold. Positive measure is stronger than .
The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.
The classical route bounds the norm of a distance measure via spherical averages of Fourier transforms (Mattila), and every improvement so far has come from finer restriction or decoupling estimates, which stall above . In higher dimensions there is a structural obstacle: radial projections of an -dimensional source cannot gain dimension above , so for one cannot assume radial projections have densities, and the angular input the Fourier argument needs must be built as cap bounds on directional fibres with arbitrarily small losses. Converting such fractal angular laws into a distance estimate requires a belt (rather than cap) estimate whose annular power is exactly balanced at , and a recursive multiscale accounting whose costs must be paid by a potential across two separated depths.
EuclideanSpace ℝ (Fin d), so dist is the Euclidean distance.dimH E : ℝ≥0∞ is Mathlib's Hausdorff dimension; the hypothesis is (d : ℝ≥0∞) / 2 < dimH E, strict.0 < volume {r : ℝ | ∃ x ∈ E, ∃ y ∈ E, dist x y = r} with Lebesgue volume on ℝ; compactness of makes this set compact.PlanarFalconer.distanceSet on EuclideanSpace ℝ (Fin 2) with 1 < dimH E.A complete development needs Frostman's lemma, energy and Fourier characterizations of dimension, Mattila's spherical-average criterion, stationary phase for spherical oscillatory integrals, and the Orponen–Shmerkin planar incidence theorem (used as an external input). Contributions formalizing Lemma 5.5 (the classical distance threshold ), Theorem 4.1 (linear projection gain), Theorem 4.2 (planar discretized Furstenberg estimate), Proposition 5.10 (starting pair measures), Proposition 8.1 (graph estimate) and Theorem 10.4 (single-profile angular bound) are welcome.
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.