Math and TheoryLean proofs
Every result in the collection comes with Lean 4 proofs of its stated formal scope. This page lists, in order of significance, what each formalization proves, the checked theorem names or library roots, and where the sources are. The verification guide gives the commands for checking them.
- Selected result:
The small-coefficient upper half of the Keller–Klein conjecture
The theorem for every finite vector of real coefficients, with the exact count of sign vectors and Mathlib's standard normal distribution function, is formalized in 62 Lean modules, including Prawitz smoothing, the characteristic-function envelopes and both analytic zones. Ivanisvili's Theorems 1.1 and 10.9, needed for the full conjecture, are external computer-assisted results and are not formalized.
Library roots
- Selected result:
The exact last-gradient bound for constant-step gradient descent in the strongly convex case
The actual-function upper bound and normalized actual-function attainment are formalized, including every horizon and closed parameter boundary. Sharpness for arbitrary L > 0 and radius R > 0 is proved by rescaling in the manuscript, without a separate Lean wrapper.
Library roots
- Selected result:
A narrow interval for the universal multiplier step of two-block ADMM
The consensus convergence theorem for 0 < τ ≤ 377359/200000, the arbitrary-rank and full-rank affine-constraint theorems, all seven finite-memory interval certificates and the periodic orbit in R^128 for τ ≥ 1.8868840… are formalized in 301 Lean modules. The scalar theorem, individual objective-value limits, the reduction from proper closed convex functions to proximal attainment, and penalty rescaling are conventional.
Library roots
- Selected result:
No universal finite collapse of the upper PPT entanglement-cost hierarchy
The strict separation at every adjacent level, for the actual semidefinite programs with unrestricted complex auxiliaries and positive-definite trace-one states with positive Bell coefficients, and the absence of a universal finite collapse are formalized in 17 Lean modules. The operational exact-cost and tensor-multiplicativity consequences use published theorems of Lami, Mele and Regula.
Library roots
- Selected result:
Depth-one Artin–Schreier defect towers are composita
Both implications are formalized in two Lean projects. The Lean 4.35 project states the conjecture for every finite Artin–Schreier tower over a base whose valuation ring is henselian in Mathlib's sense, with depth one defined as the least length of a complete Mac Lane–Vaquié chain over all primitive generators; it compares these chains with Okutsu sequences at length one only. The Lean 4.19 project states depth one through Okutsu sequences in the algebraic closure of K inside the Hahn field.
Library roots
lean/AdditiveGalois.lean lean/ClosureTransport.lean lean/FirstAccumulation.lean lean/FirstBlock.lean lean/FirstBlockContainment.lean lean/HahnASRoot.lean - 15 more
Library roots
- Selected result:
Matrix-pencil rank distance as an explicit completion problem
The explicit equivalence over every infinite field, for arbitrary rectangular pencils, every border size and distinct anchors including eigenvalues, and the common-summand cancellation are formalized in two Lean projects. The identification with the barred pencils of the conjecture uses a published linearization theorem and is not formalized.
Library roots
Library roots
- Selected result:
Counterexamples to the Kronecker-square lower bound for nonnegative rank
The whole family is formalized in Lean, with nonnegative rank minimized over all real nonnegative factorizations, together with a literal negation of the conjecture over all finite rectangular nonnegative real matrices. The width-109 factorization of the order-11 witness is also checked in exact rational arithmetic. The exact nonnegative rank of the squares is not determined.
Library roots
- Selected result:
Finite real counterexamples and spectral obstructions for q-permanent monotonicity
Lean 4.19.0 proves, for the inversion-weighted q-permanent of ordered real matrices, the endpoint identity 2D₁(VVᵀ) = C(n,2)‖f‖² − ‖G‖² for every real n × 3 matrix, soundness of the four-row integer certificate for every type list, the reduction of a negative endpoint to a rational positive-definite matrix with rational 0 < q₁ < q₂ < 1, identity padding, rank three of the frozen witness and the all-orders statement from its certificate inequality; a strict audit covers all 749 project declarations other than code-generation auxiliaries, with no native evaluation. The finite comparison for the 896-row witness is checked outside Lean by two independent exact programs, one of which determines per(B) and the wedge norms through the Chinese remainder theorem. The explicit regularization and the asymptotic and spectral theorems are conventional.
Library roots
- Selected result:
The sharp level-one Fourier weight at density one eighth
The formal proof includes arbitrary dimensions, the exact moment identities, the Hamming-distance bound, and sharpness witnesses.
Library roots
- Selected result:
Escaping Nesterov flows and iterates below critical damping
The continuous-time Hilbert-space threshold, the discrete threshold and the planar escape for 1 < r ≤ 2, including actual gradients, global solutions from rest and norm divergence, are formalized. The planar escape of the same potential for 0 < r ≤ 1, its boundedness for r > 2 and existence of solutions for r ≤ 1 are conventional.
Library roots
- Selected result:
Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity
The proof constructs local basis permutations and establishes their finite complex Hilbert-space interpretation. Arbitrary changes to an external Schmidt basis are not separately formalized.
Library roots
Sharp stability and exact cap optima for Rademacher sums
Lean 4.19.0 proves, for actual finite signed coefficient vectors and their actual minimum signed sum, the inverse theorem with its equality classification, stability at every cap with an explicit admissible comparison vector and its optimality, the exact saturated modulus with its equality cases and attainment, the fixed-flat inequalities and the sharpness witnesses: 67 audited statements in 15 new modules, replayed with nine inherited modules and the 62 earlier modules. A conditional Lean bridge derives the four-shift envelope with the analytic tail inputs as hypotheses. The probability optima have conventional proofs using the Keller–Klein, Hollom–Portier and Tomaszewski inputs and validated interval certificates on 27,972 rational boxes.
Library roots
The exact asymmetric Merino–Welsh region for finite matroids
The statement uses actual Mathlib matroids and the literal subset rank sum. It includes empty ground sets and finite ground sets in arbitrary ambient types.
Library roots
Critical hard-core influence bounds via nonbacktracking collisions
The influence bound for the actual hard-core Gibbs measure on every finite simple graph of maximum degree at most Δ, all activities up to λ_c(Δ) and all feasible pinnings is formalized in 32 Lean modules, including the regular completion and the nonbacktracking collision estimate. The Glauber-dynamics mixing corollary and the numerical observations on the constant are not formalized.
Library roots
Gyires's permanent inequality for structured matrices
The selected Comparator statements cover order-five circulants, the all-order four-block theorem, and the exceptional-vector theorem for n ≥ 2. Separate Lean packages prove the general order-six and all-order permutation-polynomial theorems. General permanent comparisons and direct-sum closure are also proved in Lean. The rank-two theorem has a complete Lean proof for orders 2 through 8. The general order-seven circulant theorem and rank-two orders 9 through 15 remain incomplete in Lean.
Checked theorems
MathAndTheory.GyiresCirculant5. gyires_ratio MathAndTheory.GyiresCirculant5. gyires_ratio_eq_iff MathAndTheory.GyiresCirculant5. gyires_denominator_pos MathAndTheory.GyiresCirculant5. gyires_homogeneous MathAndTheory.GyiresCirculant5. gyires_homogeneous_eq_iff MathAndTheory.GyiresCirculant5. strong_inequality MathAndTheory.GyiresCirculant5. strong_inequality_eq_iff MathAndTheory.GyiresCirculant5. strong_margin MathAndTheory.GyiresCirculant5. strong_margin_attained MathAndTheory.GyiresCirculant5. strong_margin_sharp MathAndTheory.GyiresFourBlock. contractions MathAndTheory.GyiresFourBlock. margin MathAndTheory.GyiresFourBlock. gyires MathAndTheory.GyiresFourBlock. gyires_eq_iff MathAndTheory.GyiresExceptional. strong MathAndTheory.GyiresExceptional. gram_eq_iff MathAndTheory.GyiresExceptional. gyires MathAndTheory.GyiresExceptional. gyires_eq_iff
Periodic obstructions to small-extrapolation Chambolle–Pock
The universal three-cycle threshold and its attainment, the seven-cycle with its open basin, the four-dimensional family for every κ > 2 and the quadratic eigenmode comparison are formalized in 21 Lean modules. The limsup consequence, numerical observations of larger θ-intervals and basin sizes, and the finite-dimensional matrix-convergence bridge are conventional or observational.
Library roots
Graphs with five harmonic boundary vertices, subcubic graphs with six, and minimum-boundary two-trees
Lean 4.35.0 proves, for finite simple graphs with certified shortest-path distances and the original strict boundary inequality, that a nonboundary degree-three vertex whose deletion leaves the graph connected forces six boundary vertices; the one-point gluing and block-accounting identities; the 14-vertex sharpness example; all 835 integer infeasibility systems of the local certificate; the bipartite subcubic boundary characterization; a sharp rooted metric truncation theorem; and the grammar weight bounds and polynomial identities for two-trees. A strict audit covers all 15,771 project declarations. The cone coverage, capping reduction, diameter-three argument, subcubic interior reduction, block decomposition, grammar correspondence and catalogue enumerations are conventional proofs and exact computations, replayed by the package checkers and by independent enumerations.
Library roots
Structural selfadhesivity does not imply a numerically selfadhesive realization
Both parts are formalized in Lean for arbitrary real polymatroids, with actual subset and relabeling semantics, all 32 overlap witnesses and the exact separating identity. The minimality suggested by Boege's four-variable computation is a literature consequence and is not formalized.
Library roots
Exact three-uniform Berge-path saturation numbers and a counterexample to a conjectured formula
Lean 4.35.0 proves, for actual three-uniform hypergraphs, Berge paths and saturation under every absent triple, that t disjoint loose d-cycles with two isolated vertices are Berge-P_{d+2}-saturated for every d ≥ 3, that the explicit 34-vertex hypergraph is Berge-P₁₀-saturated with 16 hyperedges, and that the three-uniform case of the conjecture fails for every m ≥ 10. The matching lower bound, the exact formula and the uniqueness of extremal hypergraphs have conventional proofs that use two results of the source paper.
Library roots
Exact Berge saturation numbers of the subdivided star in every uniformity and its minimality among trees
Lean 4.35.0 proves, for actual r-uniform hypergraphs on Fin n, Berge copies of B_a with injective vertex and hyperedge maps, and saturation under every absent r-set, that the saturation number, defined as the least size of a saturated hypergraph on Fin n, equals ⌊a(n + 1)/((r − 1)a + 1)⌋ for all a, r ≥ 3 and n ≥ (r − 1)a + 1, together with the near-minimum structure theorem; a strict audit covers all 570 project declarations. The smaller orders, the sharpness constructions and the minimality among trees have conventional proofs.
Library roots
Strong minimum-rank multiplicativity from unextendible product constraints
The rank-doubling theorem with an arbitrary partner, strong minimum-rank multiplicativity, the Tiles support and normalized density operators, and the exact all-copy Schmidt-number equivalence are formalized in 22 Lean modules. The zero-error LOCC cost, the rank-four two-qutrit PPT class and the channel interpretation combine the formal theorem with published results.
Library roots
A quartic entropy deficit for random rankings
The proof includes all finite sizes and actual position-valued permutations. It assumes neither independent comparisons nor transitive preferred directions.
Library roots
Order-polynomial positivity for width-two posets with a chain of at most five elements
Lean 4.35.0 checks the chamber certificates for a short chain of size at most four: for each of the 22 chambers the kernel (decide +kernel, no native_decide) verifies that squares and a nonnegative remainder add up exactly to the certified gap polynomial, and Lean proves that each such polynomial is nonnegative on the closed orthant of any linearly ordered field and dominates (a − 1)! times the sum of the comparable gaps, and that the chambers are exactly the Dyck words. The identification of the gap polynomials with the linear coefficient of the order polynomial (descent–rook correspondence, degree bound, determining set and point identities), the 42 chambers for a = 5 and the reduction to the linear coefficient have conventional proofs or certificates checked by an independent standard-library program.
Library roots
Three-uniform Berge-C₄ saturation: linear bounds with coefficients 5/8 and 3/4, the cone spectrum and exact small values
Lean 4.35.0 proves, for actual three-uniform hypergraphs on Fin n, Berge-C₄s with distinct vertices and distinct hyperedges, and saturation under every absent triple, that for every n ≥ 9 a saturated hypergraph with ⌈(3n − 9)/4⌉ hyperedges exists, together with the general rooted-gluing theorem, the exact values for n ≤ 5 and the upper bounds for n = 6, 7, 8; explicit pieces are kernel-checked without native_decide. The lower bound, the cone classification and spectrum and the flexible-root theorem have conventional proofs, and the values for 6 ≤ n ≤ 13 rest on exhaustive certificates checked by an independent C++ verifier.
Library roots
Ultra-log-concavity of domination sequences of powers of paths and cycles
Actual finite graph domination counts for powers of paths and cycles. No theorem for arbitrary graphs or real-rootedness is asserted.
Library roots
The multi-marginal converse of Minty's theorem fails in the plane
The whole argument is formalized in Lean for the actual two-point swap condition and maximality among all subsets of (ℝ²)³: the finite obstruction over arbitrary real tuples, the Zorn extension and the nonconvexity of the sum image. The reformulation through firmly nonexpansive maps is proved in the text only.
Library roots
The upper saturation spectrum of Berge triangles in triple systems
Lean 4.35.0 proves that paired products are Berge-triangle-free and saturated with p(n−2p) edges, that for every n ≥ 8 the explicit system J(⌊n/4⌋, n−2⌊n/4⌋) is saturated, is not a paired product and has exactly ⌊(n−1)²/8⌋ edges, and the arithmetic of the window, including the explicit deficits and at least ⌊n/4⌋ − ⌊√(2n)⌋/2 − 1 sizes there that are not of the form p(n−2p). It derives the upper spectrum and the maximum ⌊(n−1)²/8⌋ for saturated nonproducts from the containment theorem, which enters as a hypothesis and has a conventional proof, checked computationally for small orders.
Library roots
Blocking sets of PG(2,13) invariant under a fixed-point-free Singer subgroup meet some line in five points
Lean 4.35.0 models PG(2,13) with Mathlib's projectivization of F₁₃³ and proves that the Singer cycle has order 183, that its subgroup H of order three fixes no point, that the 21-point witness is an H-invariant minimal blocking set with largest line intersection five, the reduction of every H-invariant set to 61 orbit conditions, and the nonexistence of a solution with intersections at most four, by a kernel-checked search with a soundness proof; the main theorem is IsLeast admissibleCaps 5. The conjugacy of all fixed-point-free subgroups of order three is conventional.
Library roots
A rank bound for represented totally positive unit squareclasses
The bound for every algebraic totally real field, including infinite extensions, every O_K-submodule with integral norms in a finite-dimensional totally positive definite space, and actual units of the ring of integers is formalized in 11 Lean modules. The derivation from finite reflection groups, sharpness and the universality corollary are conventional.
Library roots
Logarithmic influence bounds and variance counterexamples for Boolean decision-tree covariance
For finite Boolean decision trees with no repeated coordinate on a root-to-leaf path, a logarithmic influence bound controls signed and absolute tree covariance. A known family attains equality at powers of two. Exact read-3 examples disprove the proposed coefficient-one variance replacement, including an example in which every query is relevant. No Fourier entropy theorem is formalized.
Library roots
Diagonal concavity does not imply concavity for sums of elementary symmetric polynomials
For positive M, let f=1+Mσ₁+σ₂+Mσ₃+σ₄ in four variables. Its fourth root is concave on the positive diagonal exactly when M≥1. It is concave on the full positive orthant exactly when M=1. Every M>1 therefore disproves Lachaume’s diagonal criterion with strictly positive coefficients.
Checked theorems
ConcavityChallenge.result
Counterexamples to a best-of-n win-rate bound at every budget
For every n≥2 and δ>0, there is a finite positive reference distribution whose largest atom is at most δ and whose best-of-n policy violates the proposed divergence–win-rate curve. A four-response best-of-two example gives exact probabilities and a strict logarithmic certificate. The proof uses finite interval bounds and gives a quantitative positive gap. It does not determine the sharp replacement curve.
Checked theorems
BestOfNChallenge.result BestOfNChallenge.every_budget_small_atoms
Real positive-definite counterexamples to extended q-permanent monotonicity
For every real parameter q>1, a real symmetric positive-definite matrix has a negative q-permanent derivative at q. An explicit matrix of order five decreases from q=14 to q=15. Correlation matrices with no zero entries and integer-entry examples are also obtained. The dimension can depend on q. The real-symmetric question on [−1,1] remains outside the result.
Checked theorems
QPermanentProblem.finite_counterexample QPermanentProblem.extended_conjecture_false QPermanentProblem.negative_derivative_at_every_parameter QPermanentProblem.dense_correlation_counterexamples QPermanentProblem.integer_counterexamples
Counterexamples to a late-iterate ordering conjecture for generalized Hofstadter functions
For every k≥4, some input n satisfies Fₖ^(2k+1)(n)>Fₖ₊₁^(2k+2)(n). The proof constructs inverse iterates whose exact gap is k−3. The finite witness F₄⁹(132)=8>7=F₅¹⁰(132) gives the first instance. The result concerns infinitely many parameters, not infinitely many violating inputs for each fixed parameter.
Checked theorems
HofstadterChallenge.result
A rational five-cycle for two-block ADMM with multiplier step below two
Seven modules and eleven endpoint audits cover the orbit, minimizers and optimizer. Analytic regularity of the finite strongly convex extension retains a conventional proof.
Library roots
Sharp root log-concavity of alternating Motzkin sums
Let Tₙ be the alternating sum of Motzkin numbers through index n. The sequence Tₙ^(1/n) is strictly log-concave on its tail starting at five. The inequality reverses at center five, so no earlier tail is log-concave. This strengthens Zhao’s proposed tail starting at nine. The source recurrence and finite sum are linked in Lean.
Checked theorems
MathAndTheory.Motzkin. Palomar. source_defined_result
Sharp log-concavity for alternating Motzkin sums
The arbitrary-real recurrence theorem and scaled corollary, including zero forcing, are formalized. Concrete sequences, uniform-family applications, root transfer and threshold classification retain conventional proofs.
Library roots
Sharp universal Rényi threshold for iid sums on finite Sidon sets
The finite-support iid theorem, zero probabilities and critical endpoint are formalized. Comparison with unverified source definitions is conditional.
Library roots
Unbounded coalesced-mass certificates for resolution trees
The internally defined resolution-tree functional and proof class are formalized. No unconditional identification with an external conjecture or a regular proof class is claimed.
Library roots
Ordered-instance allocation transfer with exact extra-copy preservation
The transfer theorem is formalized. Existence of a fair allocation before transfer is outside the result; external source comparison is provisional.
Library roots
Leaf deletion can move the unique mode of a tree domination polynomial by two
The fixed tree, deletion, actual domination counts and unique-mode movement are formalized. External question identity and historical priority remain provisional.
Library roots
A sharp universal skewness bound for unicyclic currents
The interval for actual tilted-matrix derivatives and a local branch is formalized. Identification with long-time stochastic cumulants and sharpness have conventional proofs. Lean does not construct a continuous-time sample-path probability space or a separate optimizing-sequence theorem.
Library roots
Exact conditional contraction for Pauli channels and depolarization in every dimension
The exact conditional hockey-stick contraction coefficients are formalized for actual finite-reference density states, every stochastic Pauli qubit channel, the full physical signed depolarizing family in every dimension d ≥ 2, and every γ ≥ 1. Channel constructors, unrestricted upper bounds and matching supremum witnesses are included. Unital-qubit normal-form existence is cited; erasure-simulation and ensemble-guessing consequences retain conventional proofs.
Library roots
Exact three-setting correlation bounds at fixed steering centre
Actual two-qubit density matrices, canonical filters, Pauli correlations, the exact least upper bound, attainment and nonattainment, and fully entangled fraction are formalized. The steering-ellipsoid and optimized CJWR measurement interpretations use cited external correspondences; general steerability is outside the result.
Library roots
A positive constant-recursive sequence with nonquasipolynomial power ranks
The main and arbitrary-rank companion theorems are formalized. Generating-function and polynomial corollaries retain conventional proofs.
Library roots
A sum-of-squares proof of the four-qubit Higuchi–Sudbery entropy bound
The proof uses all sixteen complex amplitudes, actual reduced-matrix eigenvalues, an exact sum-of-squares identity, and an explicit maximizing state.
Library roots
The three-state root-fidelity entropy bound
The unrestricted three-state ensemble theorem is formalized for actual positive semidefinite complex matrices of trace one, nonnegative weights summing to one, spectral entropy and nuclear-norm root fidelity. Credited QICLean foundations and prior-work adapters retain their attribution.
Library roots
A 64-point spectral tile in F₂⁹ with no periodic complement
Spectrality with an actual basis of all complex functions on E, the tiling E ⊕ T = F₂⁹, aperiodicity of E, the exclusion of every periodic and every subspace complement, the classification of all complements as the 512 translates of T, and the failure of the periodic tiling property for F₂⁹ are formalized in 16 Lean modules. Minimality of dimension nine depends on an external dimension-eight theorem and is not formalized.
Library roots
Sharp escape of complex domination roots in square flowers
All numbered manuscript conclusions are formalized in seventy modules with 258 endpoint audits. Historical novelty and exact external-source correspondence remain provisional.
Library roots
A three-state thermal counterexample to a heat-current kurtosis conjecture
A three-state two-temperature thermal rate model satisfies local detailed balance and has an exact negative fourth-to-second cold-heat spectral cumulant ratio. Lean checks the finite matrices, complex spectrum, a smooth locally dominant eigenvalue branch, and the exact derivative ratio. It does not formalize the stochastic long-time identification theorem.
Lean sources
An entropy increase for a structurally disassortative DomiRank graph
A connected graph with 14 vertices and 32 edges has negative degree–log-degree edge covariance. All resolvent scores are positive on [251/1000,63/250] inside the stable domain. Its entropy nevertheless increases by more than 1/10000 in natural-logarithm units. This refutes the source’s assertion for every positive-score interval.
Checked theorems
DomiRankProblem.counterexample
An unbounded obstruction to projection AM–GM in Loewner order
Lean verifies a rational three-projection matrix obstruction and a parameterized obstruction for every real multiplier in dimension three; rank-one, positive-definite mean, rational all-multiplier choices, and the standard minimal-factor observation have complete conventional proofs.
Library roots
A pure-state matched-basis information inequality violation in dimension five
The dimension-five identical-local-basis theorem is formalized. The prime-family extension is conventional; arbitrary or independently optimized basis choices are outside the result.
Library roots
A polygon enclosure fails for sums of normal matrices
Actual normal matrices, determinants, straight-segment exterior and component exclusion are formalized. Correspondence with an external source conjecture is conditional.
Library roots