Coverage

Each library is a row. A mapped library has one row per source it is mapped from; a library not mapped yet says what its map will be made of.

Decomposed (41)

Mathlib / Mathlib overview

512 of 512 list items in Mathlib, one article per concept.

508 statements

Category · Small category · Functor · Natural transformation · Yoneda embedding · Isomorphism · Adjunction · Monad · Comma category · Limits · Presheafed space · Sheafed space · Monoidal category · Cartesian closed · Abelian category · Grothendieck topology · Natural number · Integer · Rational number · Continued fraction · Real number · Extended real number · Complex number · \(p\)-adic number · \(p\)-adic integer · Hyper-real number · Group · Group morphism · Group action · Class formula · Burnside lemma · Subgroup · Index of a subgroup · Normal subgroup · Simple group · Subgroup generated by a subset · Quotient group · First isomorphism theorem · Second isomorphism theorem · Third isomorphism theorem · Abelianization · Free group · Presented group · Schreier's lemma · Cyclic group · Nilpotent group · Permutation group of a type · Cayley's theorem · Alternating group · Alternating groups on 5 letters or more are simple · and 458 more

Mathlib / Undergraduate mathematics

399 of 566 list items in Mathlib, one article per concept.

191 statements

Product of vector spaces · Vector subspace · Sum of subspaces · Direct sum · Complementary subspaces · Linear independence · Generating sets · Existence of bases · Range of a linear map · Kernel of a linear map · Algebra of endomorphisms of a vector space · Transpose of a linear map · Orthogonality · Rank of a linear map · Rank of a set of vectors · Determinant of vectors · Determinant of endomorphisms · Special linear group · Orientation of a \(\R\)-vector space · Change of basis · Rank of a matrix · Gaussian elimination · Annihilating polynomials · Invariant subspaces of an endomorphism · Generalized eigenspaces · Jordan-Chevalley-Dunford decomposition · Irreducible representation · Schur's lemma (Linear representations) · Matrix exponential · Direct product of groups · Order of an element · Stabilizer of a point · Orbit · Quotient space (Basic definitions) · Conjugacy classes · Complex roots of unity · Primitive complex roots of unity · Decomposition into transpositions · Decomposition into cycles with disjoint support · Signature · General linear group (Classical automorphism groups) · Orthogonal group · Special orthogonal group · Unitary group · Special unitary group · Maschke theorem · Ring structure \(\Z\) · Product of rings · Invertible elements · \(\Z\) is a Euclidean ring · and 141 more

Mathlib / Freek Wiedijk's 100 theorems

79 of 100 list items in Mathlib, one article per concept.

64 statements

The Irrationality of the Square Root of 2 · The Denumerability of the Rational Numbers · Pythagorean Theorem · The Area of a Circle · Euler’s Generalization of Fermat’s Little Theorem · The Infinitude of Primes · Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Fundamental Theorem of Integral Calculus · Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · De Moivre’s Formula · Liouville’s Theorem and the Construction of Transcendental Numbers · The Non-Denumerability of the Continuum · Formula for Pythagorean Triples · Schroeder-Bernstein Theorem · Leibniz’s Series for Pi · Sum of the Angles of a Triangle · The Ballot Problem · Fermat’s Last Theorem · Divergence of the Harmonic Series · The Solution of a Cubic · Arithmetic Mean/Geometric Mean · Solutions to Pell’s Equation (Freek Wiedijk's 100 theorems) · Minkowski’s Fundamental Theorem · Sum of the Reciprocals of the Triangular Numbers · The Binomial Theorem · The Partition Theorem · The Solution of the General Quartic Equation · Dirichlet’s Theorem · Wilson’s Lemma · The Number of Subsets of a Set · Königsberg Bridges Problem · Product of Segments of Chords · Heron’s Formula · Formula for the Number of Combinations · Bezout’s Theorem · Theorem of Ceva · Cantor’s Theorem · L’Hopital’s Rule · Isosceles Triangle Theorem · Sum of a Geometric Series · Sum of an arithmetic series · Greatest Common Divisor Algorithm · The Perfect Number Theorem · Ascending or Descending Sequences (Erdős–Szekeres Theorem) · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Fourier Series · Sum of kth powers · The Fundamental Theorem of Arithmetic · Divergence of the Prime Reciprocal Series · Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) · and 14 more

Mathlib / 1000+ theorems

218 of 1,199 list items in Mathlib, one article per concept.

124 statements

Ax–Grothendieck theorem · Boolean prime ideal theorem · Kleene's recursion theorem · König's theorem (set theory) · Szpilrajn extension theorem · Well-ordering theorem · Łoś' theorem · Erdős–Ko–Rado theorem · Hindman's theorem (1000+ theorems) · Multinomial theorem · Tutte theorem · Birkhoff's representation theorem · Bourbaki–Witt theorem · Cantor's isomorphism theorem · Hahn embedding theorem · Kleene fixed-point theorem · Knaster–Tarski theorem · Beatty's theorem · Dirichlet's approximation theorem · Dirichlet's unit theorem · Fermat's little theorem · Glaisher's theorem · Lucas's theorem · Mahler's theorem · Niven's theorem · Ostrowski's theorem · Pentagonal number theorem · Von Staudt–Clausen theorem · Zeckendorf's theorem · Chevalley–Warning theorem (1000+ theorems) · Integral root theorem · Mason–Stothers theorem · Primitive element theorem · Rational root theorem · Schwartz–Zippel theorem · Going-up and going-down theorems · Jacobson density theorem · Krull's principal ideal theorem · Lasker–Noether theorem · Vieta's formulas · Wedderburn's little theorem · Binomial inverse theorem · Birkhoff–Von Neumann theorem · Dimension theorem for vector spaces · Gershgorin circle theorem · Rank–nullity theorem · Sylvester's determinant theorem · Focal subgroup theorem · Wedderburn–Artin theorem · Lie's theorem · and 74 more

Fermat's Last Theorem (Imperial)

172 blueprint nodes in Lean, one article per node.

172 statements

FermatLastTheorem.of_odd_primes · fermatLastTheoremThree · FermatLastTheorem.of_p_ge_5 · FreyPackage · FreyPackage.of_not_FermatLastTheorem_p_ge_5 · Frey · Mazur · Wiles,Taylor–Wiles, Ribet,… · FreyPackage.false · FLT · hardly_ramified · Frey_curve_hardly_ramified · hardly_ramified_reducible · Wiles_Frey_again · hardly_ramified_lifts · hardly_ramified_spreads_out · hardly_ramified_mod3_reducible · hardly_ramified_3adic_reducible · ZHat · ZHat.commRing · ZHat.nontrivial · ZHat.charZero · ZHat.e · ZHat.e_def · ZHat.e_not_in_Int · ZHat.torsionfree · ZHat.multiples · QHat · QHat.canonicalForm · QHat.IsCoprime · QHat.lowestTerms · QHat.injective_rat · QHat.injective_zHat · QHat.rat_meet_zHat · QHat.rat_join_zHat · Qhat.unitsrat_meet_unitszHat · QHat.unitsrat_join_unitszHat · Hurwitz · Hurwitz.ring · Hurwitz.starRing · Hurwitz.norm · Hurwitz.norm_eq_mul_conj · Hurwitz.norm_zero · Hurwitz.norm_one · Hurwitz.norm_mul · Hurwitz.norm_nonneg · Hurwitz.norm_eq_zero · Hurwitz.exists_near · Hurwitz.quot_rem · Hurwitz.left_ideal_princ · and 122 more

PNT+

383 blueprint nodes in Lean, one article per node.

383 statements

First prime gap · pi · pi star · li and Li · Equation (2) of FKS2 · Definitions 1, 5, FKS2 · Equation (1) of FKS2 · Equation (2) of FKS2 · Definitions 1, 5, FKS2 · Definitions 1, 5, FKS2 · Admissible bound decreasing for large x · Classic bound implies numerical bound · first-fourier · second-fourier · Preliminary decay bound I · Preliminary decay bound II · Preliminary decay bound III · Decay bound, alternate form · Decay bounds · Limiting Fourier identity · Corollary of limiting identity · Smooth Urysohn lemma · Limiting identity for Schwartz functions · Bijectivity of Fourier transform · Smoothed Wiener-Ikehara · Wiener-Ikehara in an interval · Wiener-Ikehara Theorem (1) · WeakPNT · limiting-fourier-variant · crude-upper-bound · auto-cheby · Wiener-Ikehara Theorem (2) · WeakPNT-character · WeakPNT-AP-prelim · WeakPNT-AP · RectangleBorder · RectangleIntegral · UpperUIntegral · LowerUIntegral · VerticalIntegral · DiffVertRect-eq-UpperLowerUs · existsDifferentiableOn-of-bddAbove · HolomorphicOn.vanishesOnRectangle · RectanglePullToNhdOfPole · ResidueTheoremAtOrigin · ResidueTheoremOnRectangleWithSimplePole · zeroTendstoDiff · RectangleIntegral-tendsTo-VerticalIntegral · RectangleIntegral-tendsTo-UpperU · RectangleIntegral-tendsTo-LowerU · and 333 more

Polynomial Freiman-Ruzsa

213 blueprint nodes in Lean, one article per node.

213 statements

Concavity · log sum inequality · converse log sum · Entropy · Entropy and relabeling · Jensen bound · Uniform distribution · Uniform distributions exist · Entropy of uniform random variable · Entropy of uniform random variable, II · Bounded entropy implies concentration · Commutativity and associativity of joint entropy · Conditioned event · Conditional entropy · Conditional entropy and relabeling · Chain rule · Conditional chain rule · Mutual information · Alternative formulae for mutual information · Nonnegativity of mutual information · Subadditivity · Conditioning reduces entropy · Submodularity · Alternate form of submodularity · Independent random variables · Vanishing of mutual information · Additivity of entropy · Conditional mutual information · Alternate formula for conditional mutual information · Nonnegativity of conditional mutual information · Conditionally independent random variables · Vanishing conditional mutual information · Entropy of conditionally independent variables · Negation preserves entropy · Shearing preserves entropy · Lower bound of sumset · Conditional lower bound on sumset · Independent lower bound on sumset · Copy preserves entropy · Existence of independent copies · Ruzsa distance · Distance from zero · Copy preserves Ruzsa distance · Ruzsa distance in independent case · Distance symmetric · Distance controls entropy difference · Distance controls entropy growth · Distance nonnegative · Projection entropy and distance · Improved Ruzsa triangle inequality · and 163 more

Equational Theories

137 blueprint nodes in Lean, one article per node.

137 statements

Magma · Free Magma · Lemma: For a finite alphabet \(X\), the number of… · Law · Models · Derivation · Birkhoff's completeness theorem · Equation 1 · Equation 2 · Equation 3 · Equation 4 · Equation 5 · Equation 6 · Equation 7 · Equation 8 · Equation 14 · Equation 16 · Equation 23 · Equation 29 · Equation 38 · Equation 39 · Equation 40 · Equation 41 · Equation 42 · Equation 43 · Equation 45 · Equation 46 · Equation 63 · Equation 65 · Equation 168 · Equation 206 · Equation 381 · Equation 387 · Equation 477 · Equation 854 · Equation 953 · Equation 1485 · Equation 1491 · Equation 1571 · Equation 1648 · Equation 1657 · Equation 1659 · Equation 1661 · Equation 1689 · Equation 1701 · Equation 2662 · Equation 3167 · Equation 3588 · Equation 3722 · Equation 3744 · and 87 more

Strong PNT (Math Inc)

615 blueprint nodes in Lean, one article per node.

615 statements

Log growth · Square log · Double log · Log compare · Exp rule · Real scale · Real series · Euler's formula · Real cosine · Log inverse · Cos even · Cos even · Exp form · Real cosine · Real cosine · Real cosine · Double angle · Cos square · Square expand · Trig identity · Square nonneg · Double square · Cos square · Trig positive · Trig positive · Series positive · Real part diff · Real part 2M · Inequality reversal · Real part lower bound · Real part bound · Real part >0 · Pos real nonzero · 2M minus nonzero · Absolute value positive · 2M minus mod · Real imaginary · Mod square · Shifted mod · Mod diff · Square expand · Square diff · Mod diff · Modulus diff · Modulus identity · Nonneg product · Nonneg product · Modulus compare · Modulus bound · Modulus bound · and 565 more

Tau Ceti

2,809 articles on 3,906 declarations its roadmaps' statuses name or its docstrings name as results, the forms of one result in one article.

2,809 statements

Invariant forms classify the continuous second cohomology of formal loops · The continuous second cohomology of the formal loop algebra of a simple Lie algebra is one-dimensional · The second cohomology of the loop algebra of a simple Lie algebra is spanned by the residue class of the Killing form · Whitehead's second lemma, as an equality of submodules · Whitehead's first lemma · TauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff · TauCeti.LieAlgebra.exists_eq_smul_killingForm · TauCeti.CurrentAlgebra.instCompleteSpace · TauCeti.LieModule.Cohomology.continuousSecondCohomology · TauCeti.coinduction · TauCeti.enoughInjectives_smoothModules · TauCeti.AInfinityAlgebra.minimalModel · Kadeishvili's intrinsic formality criterion · The triple Massey product is a coset of the minimal-model ternary operation · The transferred ternary operation on ([a], [a], [b]) · TauCeti.AInfinityAlgebra.transfer · TauCeti.AInfinityAlgebra.transferHomotopy · TauCeti.AInfinityCategory.transfer · The Yoneda lemma for right A∞ modules · The Yoneda lemma for right DG modules · TauCeti.AInfinityFunctor · The Hochschild differential squares to zero · TauCeti.DGTwistedObject · TauCeti.DGTwistedObject.cone · The resolution theorem · Cartan-matrix unimodularity · The graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S] · TauCeti.gradedCartanEquiv · The q-Euler matrix of a path algebra is the inverse of its conjugate-transposed graded Cartan matrix · The graded quiver q-Euler form at q = 1 is the ungraded Ext-Euler pairing · Bigraded Ext detects linear resolutions over a semisimple degree-zero part · The Cartan--Poincare identity over a semisimple degree-zero part · The graded Cartan matrix in a projective basis bP and a module basis bM · The graded projectives A eᵢ form a basis of K₀^gr(proj A) · TauCeti.GradedProjectiveResolution.IsLinear · Equivalence invariance of the resolution theorem · The graded first-arrow Euler formula · The graded Ringel formula on Grothendieck classes · The weighted graded Cartan coefficient formula · The Jacobson–Morozov theorem · The Jacobson–Morozov theorem for embeddings · Kostant's conjugacy theorem · The transverse decomposition L = [L, e] ⊕ ker (ad f) · The simple root values of a dominant neutral element lie in {0, 1, 2} · The dimension of a centralizer and of [𝔤, x] · TauCeti.centralizerHopfIdeal · LieAlgebra.IsCentralizerRegular · The Slodowy slice e + ker (ad f), as an affine subspace of L · The contracting action of Kˣ on L attached to an sl₂ triple (h, e, f) · Morozov's lemma · and 2,759 more

Formal Frontier / Adic modules

1 highlight of its formalization.yaml whose declarations the scan finds in the linked file, one article each.

1 statement

Middle exactness of completion for a Noetherian middle module

Formal Frontier / Algebraic groups

5 highlights of its formalization.yaml and 1 headline result whose declarations the scan finds in the linked file, one article each.

6 statements

Closed linear embeddings of affine algebraic groups · Point representations and comodules · Finite-dimensional subcoalgebra containment · Finite Hopf algebras and right Hopf modules · Bidual coactions and the antipode square · Surjectivity and faithfully flat coordinates

Formal Frontier / Coherent modules

4 highlights of its formalization.yaml and 72 headline results whose declarations the scan finds in the linked file, one article each.

76 statements

Coherence via kernels of maps from finite free modules · Finiteness, projectivity and flatness under injective tensor units · Internal Krull–Schmidt decompositions and cancellation · Coherence of square-zero extensions and finite-support idealizations · Additive intertwining by ranges · Fibrewise additive intertwining · Finite coarsening of complete orthogonal idempotents · Dual endomorphisms · Tensor–dual Frobenius criterion · Annihilator quotients with two scalar actions · Noetherian semilinear Hom · Hom and End of matrix columns · Projective matrix-column semimodules · Left ideals of finite matrix semirings · Coherence of finite matrix rings · Left-regular elements in left Artinian rings · Closed semimodule categories · Kernels over semirings · Sums of nilpotent left ideals · Inverse images with nilpotent kernel · Relative generation by nilpotent ideals · Extension of products and powers of left ideals · Annihilators after localization · Coatomicity of two-sided ideals · Radical colons and pointwise annihilators · Finitely generated ideal colons and localization · Unit-ideal scalar families · Coprime scalar rows · Finite coprime-kernel decompositions · Finite generation under pointwise unimodular clearing · Semilinear Noetherian ascent · Artin–Rees for Noetherian modules · Submodule adic cofinality · Power-killed submodule criteria · Descent of adic cofinality · Adic cofinality on finite products · Cofinal ideal powers · Semilinear transport of adic cofinality · Krull intersection from adic cofinality · Finite generation from the first adic quotient · Finite presentation from cofinal ideal quotients · Essentially finite-type scalar extension · Coherent modules and kernels · Coherent homology · Coherence along semilinear retractions · Coherent dependent direct sums · Coherence over product coefficient rings · Finite presentation over product coefficient rings · Finite presentation along scalar towers · Coherence along quotient coefficients · and 26 more

Formal Frontier / Complex analysis

7 headline results whose declarations the scan finds in the linked file, one article each.

7 statements

Finite-dimensional differentiability implies analyticity · Differentiability–analyticity equivalence · Polydisc Cauchy formula · Polynomial boundary degree counts interior roots · Exterior polynomial root-scaling homotopy · Compact scalar-kernel operators · Detecting finite eigenspaces of compact positive squares

Formal Frontier / Dedekind ideal arithmetic

5 highlights of its formalization.yaml whose declarations the scan finds in the linked file, one article each.

5 statements

Ideal norms, factorization and principal primes · Class groups under localization · Section indices and rational-frame coordinates · Intrinsic heights of normed invertible modules · Adic fibre seminorms and integral spans

Formal Frontier / Fundamental groupoids

5 highlights of its formalization.yaml and 1 headline result whose declarations the scan finds in the linked file, one article each.

6 statements

Based van Kampen for intersection-closed open covers · The fundamental group of the circle is ℤ · Covering fibers, cosets, properness and homotopy groups · Fundamental groups of based disk attachments · Based-source and positive-degree homotopy-fiber exactness · Compactly generated compact-open currying

Formal Frontier / General linear groups

5 highlights of its formalization.yaml and 1 headline result whose declarations the scan finds in the linked file, one article each.

6 statements

Principal-unit quotients and Jacobson lifting · Square-zero unit kernels and conjugation · Nilpotent principal-unit groups · Positive principal-unit layer commutator pairings · Functorial symbols and Jacobson equivalences · Scalar unit reflection and canonical quasi-regular kernels

Formal Frontier / Graded rings

4 highlights of its formalization.yaml and 1 headline result whose declarations the scan finds in the linked file, one article each.

5 statements

Quotient Rees algebra of a regular principal ideal · Finite weighted normal forms for Rees modules · Finite generation of associated graded modules · Polynomial scalar extension over semirings · Polynomial covers and equivalences for principal ideals

Formal Frontier / Group rings

1 headline result whose declarations the scan finds in the linked file, one article each.

1 statement

Convolution support

Formal Frontier / Group theory

1 highlight of its formalization.yaml and 1 headline result whose declarations the scan finds in the linked file, one article each.

2 statements

Local compactness of homomorphism spaces · No small subgroups under open homomorphisms

Formal Frontier / Ideal completion

2 headline results whose declarations the scan finds in the linked file, one article each.

2 statements

Principal embedding · Prime ideals and Boolean-valued maps

Formal Frontier / Integral closure

4 highlights of its formalization.yaml and 3 headline results whose declarations the scan finds in the linked file, one article each.

7 statements

Integral domains over henselian local rings are local · Integral closedness descends along linear retractions · Normal-domain descent from arbitrary field scalar extensions · Prime-spectrum embeddings from powers in the image · Finiteness from powers of algebra generators · Integrality is unchanged by positive powers · Positive powers in the range imply an integral homomorphism

Formal Frontier / Iwasawa modules

1 headline result whose declarations the scan finds in the linked file, one article each.

1 statement

Pseudo-nullity and short exact sequences

Formal Frontier / Metrization

3 headline results whose declarations the scan finds in the linked file, one article each.

3 statements

Sigma-locally-finite basis criterion · Metric converse · Closed metrizable neighbourhood-cover criterion

Formal Frontier / Minimal primes

5 highlights of its formalization.yaml and 25 headline results whose declarations the scan finds in the linked file, one article each.

30 statements

Prime spectra of products of semifields · Ideals in products of division semirings · Nontrivial dependent reduced products · Krull dimension and chain cardinalities of lexicographic sums · Dimension and point ranks of finite dependent lexicographic products · Successors of finite product expansions · Dimension from finite coordinate-restriction images · Chain cardinalities of unions · Chain cardinalities of exclusive-piece unions · Krull dimension of exclusive-piece unions · Dimension comparison and arbitrary unions · Krull dimension under finite covers · Chain cardinalities of disjoint sums · Finite localization near a minimal prime · Directed suprema of relations on a fixed set · Directed unions: chain cardinality and order dimension · Chain cardinalities of lexicographic products · Chain cardinalities of lexicographic sums · Krull dimension of lexicographic products · Semimodules, annihilators and faithful actions on dependent reduced products · Common finite bases of dependent reduced products · Exactness of dependent reduced-product maps · Coordinate maps and zero-reflection of dependent filter products · Reindexing dependent filter products · Small products of dependent filter products · Centers of dependent filter products · Reduced filter germs · No zero divisors in ultrafilter products · Integral pullback of maximal spectra · Irreducible closed rectangles and topological product dimensions

Formal Frontier / Multivariate polynomials

55 headline results whose declarations the scan finds in the linked file, one article each.

55 statements

Heights of homogeneous polynomial evaluations · Homogeneous polynomial maps on projective coordinate spaces · Polynomial closed points and algebraic-closure orbits · Infinitely many maximal ideals of polynomial rings · Factorization uniqueness from a regular crossed resultant · Nonconstant coefficients of polynomial units · Polynomial units over commutative semirings · Prime coefficient extensions over commutative semirings · Maximal coefficient extensions over commutative semirings · Finite coefficient-product equations determine whole products · Radicals of coefficient-ideal extensions · Scalar annihilators and non-zero-divisors · The degree-zero homogeneous component · Coefficient ideals over commutative semirings · Square witnesses for failure of subtractivity · Powers of augmented coefficient ideals · Primary coefficient ideals · Supplied primary families and deletion irredundance · Nilpotent coefficients and irreducible polynomial spectra · Jacobson radicals of coefficient ideals · Integral elements over coefficient rings · Integral closure in arbitrarily many variables · Flatness of commutative-ring variable renaming · Canonical unique-variable degree · Injectivity and surjectivity of variable renaming · Formal smoothness of variable renaming · Smoothness of variable renaming · Formal unramifiedness of variable renaming · Integrality of polynomial variable renaming · Algebraicity of polynomial variable renaming · Finite presentation of commutative-ring variable renaming · Zero-variable presentations and semiring renaming · Variable renaming has an exact relative finite-type criterion · Variable renaming has an exact relative essentially finite-type criterion · Module finiteness of variable renaming has a sharper criterion · Quasi-finiteness of commutative-ring variable renaming · Finite coefficient aggregation has an exact injectivity criterion · Joint degree-and-support profiles recover bivariate coefficients only for trivial coefficients · Variable-renaming kernels have an exact presentation and finite-generation criterion · Fraction-ring renaming is surjective, equivalently integral, exactly when it covers all variables · Omitted variables are algebraically independent over the source fraction ring · Omitted variables form a transcendence basis over the source fraction ring · The image of evaluating one polynomial at two points · Finite simultaneous polynomial evaluation has an exact surjectivity criterion · Evaluation-kernel powers are detected by translated coefficients · Hilbert basis theorem for left-Noetherian rings · Artinian polynomial-semiring criteria · Univariate coefficient-module Noetherianity and Artinianity each characterize trivial coefficients · Radical coefficient-ideal extensions are characterized by subtractivity · Coefficient-and-variable ideals have an exact finite-generation criterion · and 5 more

Formal Frontier / Polynomial root stability

4 headline results whose declarations the scan finds in the linked file, one article each.

4 statements

Polynomial root scaling · Polynomial scaling in valuation balls · Root uniqueness in an ultrametric normed ring · Quantitative resultant-controlled factorization

Formal Frontier / Projective modules

3 highlights of its formalization.yaml and 4 headline results whose declarations the scan finds in the linked file, one article each.

7 statements

Sylvester's determinant identity for finite projective modules · Tensor-product determinants and rank powers · Projective modules lift across nilpotent ideals · Algebra-valued pairing matrices · Normalized pairing regulators · Nilpotence from characteristic polynomials · Frobenius functionals and self-injectivity

Formal Frontier / Restricted-product duality

1 highlight of its formalization.yaml whose declarations the scan finds in the linked file, one article each.

1 statement

Compact Pontryagin biduality

Formal Frontier / Ringed spaces

2 headline results whose declarations the scan finds in the linked file, one article each.

2 statements

Continuous-function spaces · Finite-regularity scalar functions

Formal Frontier / Scheme properties

1 highlight of its formalization.yaml whose declarations the scan finds in the linked file, one article each.

1 statement

Finiteness near all component generic points

Formal Frontier / Sequence growth

2 headline results whose declarations the scan finds in the linked file, one article each.

2 statements

Nat.DivisionGrowth.affine_lower_bound · Nat.DivisionGrowth.eventually_dominates

Formal Frontier / Spectral Stone duality

1 highlight of its formalization.yaml and 1 headline result whose declarations the scan finds in the linked file, one article each.

2 statements

Specialization and soberification dimensions · Closed points among generizations

Formal Frontier / Sphere topology

5 highlights of its formalization.yaml and 17 headline results whose declarations the scan finds in the linked file, one article each.

22 statements

Brouwer fixed points on complex disks · Hairy-ball theorem for the metric two-sphere · Free fundamental groups of circle bouquets · Sphere cogroups and sharp cocommutativity · Nontrivial second homotopy group of the metric two-sphere · H-space fundamental groups commute · Last-axis one-point compactification coordinates · Finite generalized loops and based sphere-map classes · Homotopy groups and the sphere-map group · Nontrivial second homotopy group of S² · Canonical antipodal quotient covering · Real projective fundamental groups and lifted endpoints · Embeddings, closed maps and neighborhoods of point-wide-pushouts · Point-relative equivalences and contractions · Factor retractions and separation of point-wide-pushouts · Charts around a common subset · Fundamental groups of factor-plus-core charts · Subfamily retractions and continuous factorization · Strict finite-stage factorization of compact homotopies · Arbitrary-index circle bouquets · Diagonal equivalence for non-antipodal pairs · Covering-space lifts of simplices

Formal Frontier / Toric ideals

3 highlights of its formalization.yaml whose declarations the scan finds in the linked file, one article each.

3 statements

Uniform monomial-evaluation kernels · Monomial conductors · Own-fraction normalization of monomial algebras

Formal Frontier / Valuation integers

5 highlights of its formalization.yaml whose declarations the scan finds in the linked file, one article each.

5 statements

Prescribed finite separable residue extensions · Residue degree bounded by field degree · Unique residue and field homomorphism lifts · A sharp Hensel criterion at arbitrary valuation rank · Unit norms over Henselian valuation domains

Formal Frontier / Vector bundles

4 highlights of its formalization.yaml and 1 headline result whose declarations the scan finds in the linked file, one article each.

5 statements

Compatible Hermitian metrics · Orthogonal complements for a supplied metric · Fiberwise linear isomorphism criterion · Sigma-compactness of a fiber bundle · Total-space continuity of semilinear maps from finite local bases

Formal Conjectures

1,814 problem files that state a research or textbook statement, one article each, with a card per statement.

1,814 statements

Erdős Problem 1 · Erdős Problem 2 · Erdős Problem 3 · Erdős Problem 4 · Erdős Problem 5 · Erdős Problem 6 · Erdős Problem 7 · Erdős Problem 9 · Erdős Problem 10 · Erdős Problem 11 · Erdős Problem 12 · Erdős Problem 13 · Erdős Problem 14 · Erdős Problem 15: Convergence of Series with Primes · Erdős Problem 16 · Erdős Problem 17 · Erdős Problem 18 · Erdős Problem 19 · Erdős Problem 20 · Erdős Problem 21 · Erdős Problem 22 · Erdős Problem 23 · Erdős Problem 24 · Erdős Problem 25: Logarithmic density of size-dependent congruences · Erdős Problem 26 · Erdős Problem 28 · Erdős Problem 29 · Erdős Problem 30 · Erdős Problem 31 · Erdős Problem 32 · Erdős Problem 33 · Erdős Problem 34 · Erdős Problem 35 · Erdős Problem 36 · Erdős Problem 38 · Erdős Problem 39 · Erdős Problem 40 · Erdős Problem 41 · Erdős Problem 42: Maximal Sidon Sets and Disjoint Difference Sets · Erdős Problem 43 · Erdős Problem 44: Extending Sidon Sets · Erdős Problem 45 · Erdős Problem 46 · Erdős Problem 47 · Erdős Problem 48 · Erdős Problem 49 · Erdős Problem 50 · Erdős Problem 51 · Erdős Problem 52 · Erdős Problem 53 · and 1,764 more

Lean Pool

334 project cards, one article per card.

334 statements

A 21-state Turing machine for Goldbach's conjecture · A formalization of Borel determinacy in Lean · Craig interpolation and Beth definability for propositional dynamic logic · Craig Interpolation for Gödel-Löb logic via coalgebraic proofs · DomainTheory · First Order Language of ZF Set Theory · Global completeness of one-sorted definedness-free matching logic · Gödel's First and Second Incompleteness Theorems · Infinitary logic and countable model theory · The Kunen inconsistency theorem · Lentil: Temporal Logic of Actions in Lean 4 · Nash-Williams fronts and 2-better-quasi-orders · New Foundations refutes the Weak Partition Principle · The nonmeagre lower bound for the rearrangement number · Oracle Computability and Turing Degrees · Ordered resource algebras and the Iris recursive domain model · Partial Combinatory Algebras · PCF Theory · Pointwise provable equality and the failure of composition · Strengthened V0 Bounded Arithmetic Interfaces · ZFLean · A proof of the Regts–Sevenster conjecture, formalized · Asymptotically attaining the Moore bound · Balanced and vertex-distinguishing edge colourings · BKLO simultaneous perfect matchings and spread matchings · The Bollobás–Nikiforov conjecture · Boolean Isoperimetry and Conway--Guy Coherent Gaps · Brooks' theorem for subcubic graphs · Chebyshev Quotients and Demazure Multiplicities · Chip-Firing with Lean 4 · Chordal graphs: minimal separators and simplicial vertices · Chvátal's conjecture and sharp Boolean correlation · Classical graph colouring through lists, orientations and spectra · Classical matching and factor theorems in finite graphs · Clique trees, subtree representations and chordal treewidth · Counterexamples to graph compactness and two-degenerate extremal bounds · Counting Critical Portraits · Demazure Operators and Lean · The density Hales–Jewett theorem and Szemerédi's theorem · Dross's fractional triangle decomposition theorem · The Erdős–Sós conjecture (Erdős Problem 548) · Even graphs are edge-disjoint unions of cycles · Extended Demazure Product on ASP Permutations · Finite hypergraph rounding and the asymptotic triangle-packing gap · Finite max-flow / min-cut · FrontierMath Ramsey Hypergraphs · Fundamental groups of finite connected graphs · Genus-Zero Pairings and Catalan Numbers · Geometric Four-Colorings of the Moser Lattice and Ring · Graph removal and extremal stability · and 284 more

Fermat's Last Theorem (Anthropic)

49 landmark theorems in the steps of PROOF-PATH.md, one article each; the other 29,462 theorems are counted, not mapped.

49 statements

Classification of Finite Simple Groups (Axiom)

The top theorem, its reduction to 9 cases and the theorem for each case, and 110 milestone modules, one article each, with their Lean statements.

121 statements

CFSG.classification_finite_simple_groups · CFSG.Assembly.Reduction · CFSG.FeitThompson.isSolvable_of_odd_natCard · CFSG.Assembly.abelian_simple · CFSG.Assembly.disconnected_involution_graph · CFSG.Assembly.low_two_rank · CFSG.Assembly.component_dichotomy · CFSG.Assembly.component_type · CFSG.Assembly.quasithin · CFSG.Assembly.rank_three_even · CFSG.Assembly.large_even · AT_alternating_automorphism_permutation · BI_Brauer_characterization · BL_block_section_column_orthogonality · BT_principal_block_Brauer_correspondence · CAT_converse · CAT_native_realization · CFSG_classification · CFSG_exhaustiveness · CLS_K_proper_simple_classification · CLS_QTKE_classification · CLS_abelian_simple_catalog · CLS_characteristic_two_classification · CLS_component_classification · CLS_component_dichotomy · CLS_component_free_centralizer_quotient_characteristic_two · CLS_component_free_involution_odd_cores_trivial · CLS_connectivity_MacWilliams_four_generator · CLS_disconnected_simple_involution_graph_classification · CLS_involution_centralizers_characteristic_two_transfer · CLS_large_even_classification · CLS_low_two_rank_classification · CLS_rank_three_even_classification · CL_LIT_AS_vol_I_background · CL_LIT_Aschbacher_1983_uniqueness_case_rank_three · CL_LIT_Aschbacher_component_type_theorem_5 · CL_LIT_Aschbacher_proper_two_generated_core · CL_LIT_Borel_Tits_local_parabolic · CL_LIT_Curtis_Tits_presentation_theorem · CL_LIT_Fischer_3T_existence_uniqueness · CL_LIT_Fischer_three_transposition_theorem · CL_LIT_GH74_sectional_two_rank_four · CL_LIT_GL83_Theorem_C_preuniqueness_rank_three · CL_LIT_GMS_Monster_uniqueness · CL_LIT_Gilman_Solomon_maximal_unbalancing_reduction · CL_LIT_Goldschmidt_strongly_closed_abelian · CL_LIT_Goldschmidt_strongly_closed_abelian_models · CL_LIT_Gorenstein_Walter_L_balance · CL_LIT_Griess_Schur_multipliers_Lie_type · CL_LIT_Monster_existence_Griess_Conway · and 71 more

Deferred (5)

Physlib

Planned map, by documented declaration: One article per documented declaration, grouped by physics area; granularity to be checked against a docstring count.

CSLib

Planned map, by documented declaration: One article per documented public declaration.

Foundation

Planned map, by documented declaration: One article per documented declaration; the Zoo's inclusion diagrams between logics as edges.

Analysis I companion

Planned map, by textbook section: One article per textbook section (the Section_X_Y modules).

OpenAI Math

Planned map, by result family: One article per result family in CONTENTS.md, joined to the 208 formalization.yaml main results.