These are summaries of selected result families, not substitutes for their full contracts. In the fitting results, d is dimension, n is sample size, α is the limit of n/d², and κ is the fourth moment. Each source link is fixed to the same released commit.
26 result families and 9 library topics. All are shown below.
Original Gaussian results
Three Gaussian ellipsoid-fitting results
The probability of a positive semidefinite fit tends to one below density 1/4 and to zero above it. Below the threshold, fits can also have trace d and fixed positive spectral bounds. Balanced positive-definite combinations of sample outer products have the opposite transition.
Hypotheses and scope. Independent standard Gaussian points in dimension d; sample sizes n(d). The fitting transition uses limsup n/d² < 1/4 or liminf n/d² > 1/4. For every alpha < 1/4, the well-conditioned result assumes limsup n/d² ≤ alpha; its spectral constants depend only on alpha.
One formal theorem bundles three mathematical results and includes measurability of their events. No claim at the critical density follows from these threshold statements. Formalization of the three main results of Misiakiewicz and Wen.
ellipsoid_fitting_main
Extensions
Universality and finite or countable mixtures
A sharp fitting transition at alpha_*(kappa), bounded-condition positive definite fits below it, and a deterministic limiting fitting error extend from independent coordinates to finite and countable mixtures of product laws.
Hypotheses and scope. Samples are independent and identically distributed; n/d² tends to alpha > 0. Within each mixture component, coordinates are independent, mean zero, variance one, and uniformly subgaussian with one constant K > 0. Every coordinate has unconditional fourth moment kappa > 1 after averaging over the mixture. Mixture families and their weights may depend on dimension.
Coordinates of a point may be dependent under the mixture. A component need not itself have fourth moment kappa. The independent-coordinate result formalizes Koehler and Sohn; the mixture extension is stated separately.
Other statements in this family
countable_theorem
Extensions
The optimal condition number
For every C > 1, the probability of an exact fit with condition number at most C has threshold alpha(C,kappa). Below alpha_*(kappa), the optimal condition number converges in probability to C_*(alpha,kappa), the inverse curve.
Hypotheses and scope. Admissible finite or countable mixtures of product laws, with common subgaussian bound K > 0 and unconditional fourth moment kappa > 1. n/d² tends to alpha > 0; convergence of the optimum assumes 0 < alpha < alpha_*(kappa).
Nothing is asserted at alpha = alpha(C,kappa). The condition number is the matrix eigenvalue ratio; the ellipsoid semiaxis ratio is its square root. At kappa = 3, alpha_*(3) = 1/4.
Other statements in this family
condition_kappa_theorem
Extensions
Robustness to small changes of law
The condition-number threshold and limiting optimum persist when the point law is within o(d⁻²) in total variation of an admissible finite or countable mixture.
Hypotheses and scope. Reference families satisfy the mixture assumptions with kappa > 1 and K > 0. d² times the total-variation discrepancy tends to zero. The threshold comparison is away from alpha(C,kappa); the optimum limit is below alpha_*(kappa).
A separate contamination example shows that O(d⁻²) cannot replace o(d⁻²) in general.
Other statements in this family
condition_kappa_robust_theorem
Extensions
Explicit dependent point laws
Paired coordinates and a single latent sign shared across all coordinates yield explicit dependent laws with sharp fitting transitions. The latent-sign theorem also gives the limiting fitting error and small-residual interpolation.
Hypotheses and scope. Paired-law parameter −1 ≤ eps ≤ 7/3. Latent-sign parameter 0 ≤ s ≤ 1, allowed to depend on dimension; the unconditional coordinate fourth moment is 9/5. Independent samples with n/d² tending to a positive density.
The condition and interpolation constants in the latent-sign result are uniform over s in [0,1].
Other statements in this family
latent_sign_theorem
Extensions
Dependence and the limits of the mixture model
For the latent-sign law, variance-tensorization constants can grow exponentially with dimension, despite exact fitting below the threshold. A continuous latent mixture can remain at total-variation distance one from every countable mixture of product laws.
Hypotheses and scope. The exponential lower-bound result concerns a fixed latent-sign parameter s > 0 in the specified latent-sign family. The matching upper-bound theorem covers 0 ≤ s ≤ 1. The continuous-mixture result concerns its explicitly constructed law; it is not a claim about every continuous mixture.
The upper tensorization bound is 2 ((1+s)/(1−3s/7))^d.
Other statements in this family
latent_tensor_theorem
Translated samples
S1 · Small Gaussian shifts preserve the optimum
The centered-Gaussian condition-number threshold and limiting optimum are unchanged by deterministic shifts small compared with sqrt(d).
Hypotheses and scope. Independent N(m_d,I_d) points; n/d² → alpha > 0. ||m_d||/sqrt(d) → 0; C > 1 for the threshold. The optimal-condition limit assumes 0 < alpha < 1/4.
Equality at the condition-number threshold is left open.
shifted_condition_theorem
Translated samples
S2 · Arbitrary Gaussian shifts: the cost of translation
Below density 1/4, positive definite fits exist and the optimal condition number is of order 1 + ||m_d||/sqrt(d). A lower bound on that scale holds uniformly over translations at every positive density.
Hypotheses and scope. Independent standard Gaussian samples translated by a deterministic sequence m_d. n/d² → alpha > 0; the existence and two-sided bounds require alpha < 1/4. No bound is imposed on the shift magnitudes.
The lower bound holds on one high-probability event for all translations. The upper/existence statement applies to each deterministic shift sequence.
shifted_gaussian_theorem
Translated samples
S3 · Above the Gaussian threshold: no PSD quadric
One high-probability event excludes every quadric whose quadratic part is positive semidefinite and nonzero, whatever its linear and constant terms. It therefore excludes a centered fit after every translation.
Hypotheses and scope. Independent standard Gaussian points; n/d² → alpha > 1/4.
The event is chosen before the quadric; this is simultaneous over all such quadrics.
shifted_quadric_theorem
Translated samples
S4 · Fitting error is unchanged by Gaussian shifts
At every positive density, arbitrary deterministic shifts preserve the limiting fitting error e_*(alpha,3). Taking the infimum over all translations has the same limit.
Hypotheses and scope. Independent standard Gaussian samples; n/d² → alpha > 0. Arbitrary deterministic shift sequences.
The density alpha = 1/4 is included for the error limit. A zero limiting error does not prove exact fitting at that density.
shifted_error_theorem
Translated samples
S5 · Symmetric mixtures exclude all PSD quadrics
Above alpha_*(kappa), symmetric mixture point laws have a positive fitting-error margin uniform over translations, and no quadric with nonzero positive semidefinite quadratic part fits all points.
Hypotheses and scope. Finite or countable admissible mixtures; kappa > 1 and a uniform subgaussian bound K > 0. The point law is centrally symmetric; individual mixture components need not be. n/d² → alpha > alpha_*(kappa).
The positive margin is chosen from kappa and alpha before K and the family. The theorem supplies measurable good events; it does not assert measurability of the existential arbitrary-quadric event.
shifted_mixture_unsat_theorem
Translated samples
S6 · Sparse shifts preserve mixture fitting
Below alpha_*(kappa), deterministic shifts supported on o(d) coordinates preserve positive definite fits with probability tending to one.
Hypotheses and scope. Finite or countable admissible mixtures; kappa > 1, K > 0, and n/d² → alpha in (0,alpha_*(kappa)). The number of nonzero shift coordinates divided by d tends to zero.
No symmetry and no bound on shift magnitudes are required. The support may change with dimension. The assertion is for each shift sequence, not one event simultaneously covering all shifts.
shifted_mixture_sat_theorem
Translated samples
S7 · Opposite shifts have the same fitting statistics
For a centrally symmetric point law, a mixture of its translates by m and −m has exactly the same joint outer-product law as the translate by m. Centered-fit probabilities, optimal condition numbers and fitting errors therefore agree.
Hypotheses and scope. Independent samples from a centrally symmetric point law. Any mixture weight in [0,1], including endpoints. The stated Gaussian and admissible-mixture asymptotic consequences use the hypotheses of S1, S2, S5 or S6 as applicable.
This does not transfer arbitrary-center quadric events or an infimum over additional translations.
shifted_sign_theorem
Applications
T1 · Gaussian matrix series
Even trace-moment bounds for symmetric Gaussian matrix series, operator-norm bounds for rectangular series, and a quantitative bound under variance and trace control.
Hypotheses and scope. An arbitrary realType; fixed real matrices and independent standard Gaussian coefficients. Symmetry is required for the trace-moment clause; moment order q is positive.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
matrix_series_theorem
Applications
T2 · Tensor packing
Bounds how many tensor pairs can have large projection onto a low-dimensional matrix subspace, given controlled correlations.
Hypotheses and scope. An arbitrary realType; vector families in Euclidean unit balls. Correlation graphs have degree at most L; correlations outside them are at most eta ≤ eps²/10000. 0 < eps ≤ 1; an orthonormal matrix family has size at most d, with d > 0.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
tensor_packing_theorem
Applications
T3 · The upper spectral edge of the GOE
The normalized GOE has expected largest eigenvalue at most 2 and Gaussian upper tails; analogous bounds control the negative edge and operator norm.
Hypotheses and scope. An arbitrary realType; the normalized Gaussian orthogonal ensemble in dimension d ≥ 1. Tail parameter t ≥ 0.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
goe_edge_theorem
Applications
T4 · The high-temperature SK spectral gap
With high probability over the Gaussian disorder, the SK heat-bath spectral gap is at least (1−2 beta)/2, with a corresponding covariance bound, uniformly over external fields and interaction scalings.
Hypotheses and scope. An arbitrary realType; 0 ≤ beta < 1/2. Interaction scaling s in [0,1]; arbitrary external fields.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
sk_gap_theorem
Applications
T5 · Orthogonal splitting of PSD matrices
Splits the identity into orthogonal projections and controls the cross-energy of a finite PSD matrix family by its pairwise trace overlaps.
Hypotheses and scope. An arbitrary realType; a nonempty finite family of positive semidefinite square matrices.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
psd_splitting_theorem
Applications
T6 · Sign/Gaussian comparison for the perceptron
The expected Ising-perceptron pressures for sign and Gaussian patterns differ by at most C M N^(−3/2).
Hypotheses and scope. An arbitrary realType; N > 0 variables and M patterns. The test function and its first three derivatives satisfy the stated uniform bounds; C depends on those bounds.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
perceptron_sign_theorem
Applications
T7 · Concentration of random SAT lifetime
The variance of the capped largest satisfiable prefix of independent uniform proper signed k-clauses is O_k(n^(1+2/k)).
Hypotheses and scope. An arbitrary realType; fixed k ≥ 3 and n ≥ k+1. The prefix length is capped at 2^(k+1)n.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
sat_variance_theorem
Applications
T9 · A limiting threshold for every fixed k-SAT
For every fixed k ≥ 3, a positive limiting density separates asymptotically satisfiable and unsatisfiable random k-SAT instances.
Hypotheses and scope. An arbitrary realType; independent uniform proper signed k-clauses on n variables. The clause count is floor(c n), for a fixed density c on either side of the threshold.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence. The theorem establishes existence of the limiting threshold, not an explicit formula for its value; equality is not asserted.
sat_threshold_theorem
Applications
T10 · Exact normalization of PSD factors
Preserves every trace pairing and factor size while bounding the traces of one factor family by m and the other by the factor dimension r.
Hypotheses and scope. An arbitrary realType; finite PSD matrix families F_i and G_j of size r, with the second index set nonempty. Every trace pairing tr(F_i G_j) is at most m.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
psd_normalization_theorem
Applications
T11 · Product smoothing of matrix squares
A product-averaged PSD matrix-valued function admits a sum-of-squares representation with quantitative weighted Fourier-coefficient bounds.
Hypotheses and scope. An arbitrary realType; finite product spaces and the stated smoothing_hyps. The matrix-valued function is positive semidefinite with trace at most B. The positive weight lambda and smoothing parameters satisfy the explicit smallness inequality in the statement.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
product_smoothing_theorem
Applications
T12 · Convergence from approximate minimum inequalities
Bounded sequences satisfying balanced approximate minimum inequalities and a neighboring-term lower bound converge, with an explicit lower estimate for the limit.
Hypotheses and scope. An arbitrary realType; nonnegative error constant A and exponent beta > 0. Beyond a fixed index, the two lower inequalities hold with error A min(r,s)^(−beta) or A s^(−beta). Boundedness is needed for convergence; the finite-index lower estimate is also proved without it.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence.
min_superadditive_theorem
Applications
T13 · Exponential PSD rank of shifted matching matrices
There is a positive integer K, uniform in 0 < rho < 1, such that every size-r PSD factorization of A_n(rho) satisfies 2^n ≤ r^K for sufficiently large even n.
Hypotheses and scope. An arbitrary realType; 0 < rho < 1; even n beyond a threshold that may depend on rho. A_n(rho) has entries |M ∩ delta(U)| − 1 + rho, indexed by odd vertex sets and perfect matchings.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence. Quantifier order: for every realType R, there is K > 0; for every rho in (0,1), there is n0. Do not claim n0 is uniform in rho. The source header distinguishes this exponential conclusion from the different superpolynomial Lean statement in the collection.
psd_rank_theorem
Applications
T14 · Exponential lower bounds for exact PSD lifts
The unshifted matching matrix, its full slack matrix and exact semidefinite lifts of the perfect matching polytope all satisfy exponential size lower bounds.
Hypotheses and scope. An arbitrary realType; all sufficiently large even n. A PSD factorization of A_n(0) or T_n(0), or an exact semidefinite lift of the perfect matching polytope.
Formalization of a credited argument from the OpenAI math collection, revision 1581d4cbd; the source header records the precise correspondence. The source header distinguishes this exponential conclusion from the different superpolynomial Lean statement in the collection.
psd_lift_theorem
No result matches these filters. Try a theorem name or a broader mathematical term.
The 37 reports count checked top-level targets, not every lemma: the original target bundles three mathematical results. This guide groups related results for navigation. The repository overview and the extension index give the larger inventory.