Analysis
Fundamental Theorem of Calculus
Under differentiability and integrability hypotheses, the oriented interval integral of a derivative equals the endpoint difference.
Existing formal mathematics
Landmark Theorems in Mathlib
Explore 121 familiar theorems at their exact Mathlib declarations, with plain-language explanations and separate local Lean rechecks.
- Selected theorems
- 121
- Coverage
- 9 subject areas
- ProofAtlas role
- Explain, link, and recheck
Detailed visual description
One luminous atlas path crosses a dark engraved landscape containing representative motifs from the expanding collection: unique factorization, modular reconstruction, orthogonal geometry, equal secant and tangent slopes, distributional convergence, contraction to a fixed point, diagonal non-surjectivity, and four-square representation.
Familiar starting points
Start with 8 theorems
These recognizable results offer routes into different parts of the collection. They are editorial starting points, not a ranking of importance or difficulty.
Algebra and complex analysis
Fundamental Theorem of Algebra
Every complex polynomial of positive degree has a complex root.
Geometry and linear algebra
Pythagorean Theorem
In a real inner-product space, the squared-norm identity for a vector sum holds exactly when the summands are orthogonal.
Probability and analysis
Central Limit Theorem
Centered, unit-second-moment independent identically distributed real random variables have normalized sums converging in distribution to the standard Gaussian law.
Topology
Tychonoff's Theorem
An arbitrary product of compact subsets is compact in the product topology.
Computability and logic
Undecidability of the Halting Problem
For every fixed input, Mathlib's predicate that an encoded program is defined on that input is not computable.
Number theory
Quadratic Reciprocity
For distinct odd primes, the two Legendre symbols are related by the quadratic-reciprocity sign.
Linear algebra and analysis
Cauchy–Schwarz Inequality
The norm of an inner product is at most the product of the two vector norms.
Complete selected collection
Browse all 121 selected theorems
Every selected theorem appears once, grouped by subject. Search by title, mathematical idea, or exact Mathlib declaration name.
121 theorems shown
Analysis
22 theoremsBanach Fixed-Point Theorem
Metric fixed-point theory
ContractingWith.exists_fixedPoint4-stage walkthroughBanach Open Mapping Theorem
Banach-space structure
ContinuousLinearMap.isOpenMapBanach–Alaoglu Theorem
Weak-* compactness
WeakDual.isCompact_closedBallBanach–Steinhaus Theorem
Banach-space structure
banach_steinhausCauchy Integral Formula
Contour integration
DifferentiableOn.circleIntegral_sub_inv_smulClosed Graph Theorem
Functional analysis
LinearMap.continuous_of_isClosed_graphFourier Inversion Formula
Fourier analysis
MeasureTheory.Integrable.fourierInv_fourier_eqFréchet–Riesz Representation Theorem
Hilbert-space duality
InnerProductSpace.toDualFundamental Theorem of Calculus
Differentiation and integration
intervalIntegral.integral_deriv_eq_sub8-stage walkthroughGrönwall's Inequality
Differential inequalities and ODEs
norm_le_gronwallBound_of_norm_deriv_right_leHahn–Banach Theorem
Extension theorems
exists_extension_norm_eqHolomorphic Open Mapping Theorem
Holomorphic mappings
AnalyticOnNhd.is_constant_or_isOpenInverse Function Theorem
Differential calculus
HasStrictFDerivAt.to_localInverseJensen's Inequality
Convex analysis
ConvexOn.map_sum_leKrein–Milman Theorem
Convexity in locally convex spaces
closure_convexHull_extremePointsLiouville's Theorem
Entire functions
Differentiable.exists_eq_const_of_boundedMaximum Modulus Principle
Holomorphic rigidity
Complex.norm_eqOn_of_isPreconnected_of_isMaxOnMean Value Theorem
Differential calculus
exists_deriv_eq_slope3-stage walkthroughPicard–Lindelöf Local Existence Theorem
Ordinary differential equations
IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAtPoisson Summation Formula
Fourier analysis
Real.tsum_eq_tsum_fourierSchwarz Lemma
Holomorphic metric estimates
Complex.norm_le_norm_of_mapsTo_ballTaylor's Theorem with Lagrange Remainder
Real analysis and differential calculus
taylor_mean_remainder_lagrange
Probability & measure
15 theoremsBayes' Theorem
Conditional probability
ProbabilityTheory.cond_eq_inv_mul_cond_mulCentral Limit Theorem
Limit theorems
ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum4-stage walkthroughChange of Variables Formula
Measure theory and integration
MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smulChebyshev Inequality
Concentration inequalities
ProbabilityTheory.meas_ge_le_variance_div_sqDominated Convergence Theorem
Convergence theorems
MeasureTheory.tendsto_integral_of_dominated_convergenceFatou's Lemma
Convergence theorems
MeasureTheory.lintegral_liminf_leFubini's Theorem
Product integration
MeasureTheory.integral_prodHölder's Inequality
Integral inequalities
ENNReal.lintegral_mul_le_Lp_mul_LqMinkowski's Lᵖ Inequality
Lᵖ spaces and integral inequalities
MeasureTheory.eLpNorm_add_leMonotone Convergence Theorem
Convergence theorems
MeasureTheory.lintegral_iSupRademacher's Theorem
Geometric measure theory and nonsmooth calculus
LipschitzWith.ae_differentiableAtRadon–Nikodym Theorem
Measure decomposition and density
MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eqSecond Borel–Cantelli Lemma
Almost-sure events
ProbabilityTheory.measure_limsup_eq_oneStrong Law of Large Numbers
Limit theorems
ProbabilityTheory.strong_law_ae_realTonelli's Theorem
Measure theory
MeasureTheory.lintegral_prod
Algebra
11 theoremsBinomial Theorem
Commutative algebra
add_powBurnside's Lemma
Finite group actions
MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_groupCauchy's Theorem for Finite Groups
Finite group theory
exists_prime_orderOf_dvd_cardFirst Sylow Theorem
Finite group theory
Sylow.exists_subgroup_card_pow_primeFundamental Theorem of Algebra
Polynomials
Complex.exists_root4-stage walkthroughFundamental Theorem of Galois Theory — Finite Case
Galois theory
IsGalois.intermediateFieldEquivSubgroupHilbert Basis Theorem
Commutative algebra
Polynomial.isNoetherianRingLagrange's Theorem
Subgroups and cardinality
Subgroup.card_subgroup_dvd_card2-stage walkthroughPrimitive Element Theorem
Field theory
Field.exists_primitive_elementStructure Theorem for Finitely Generated Abelian Groups
Abelian group structure
AddCommGroup.equiv_free_prod_directSum_zmodSylow Conjugacy and Counting Theorems
Sylow theory
card_sylow_modEq_one
Number theory
20 theoremsBasel Problem
Special values of zeta series
hasSum_zeta_twoBertrand's Postulate
Elementary prime distribution
Nat.exists_prime_lt_and_le_two_mulChinese Remainder Theorem
Modular arithmetic
ZMod.chineseRemainder4-stage walkthroughClassification of Pythagorean Triples
Diophantine equations
PythagoreanTriple.classificationDirichlet's Theorem on Primes in Arithmetic Progressions
Analytic number theory
Nat.infinite_setOf_prime_and_eq_modDivergence of the Reciprocal-Prime Series
Prime reciprocal series
Nat.Primes.not_summable_one_divEisenstein Criterion
Polynomial irreducibility
Polynomial.irreducible_of_eisenstein_criterionEuler's Totient Theorem
Modular arithmetic
Nat.ModEq.pow_totientFermat's Last Theorem for Exponent Four
Diophantine equations
fermatLastTheoremFourFermat's Little Theorem
Prime congruences
Nat.ModEq.pow_card_sub_one_eq_oneFermat's Two-Square Classification
Sums of squares
Nat.eq_sq_add_sq_iffFundamental Theorem of Arithmetic
Prime factorization
Nat.primeFactorsList_uniqueInfinitely Many Primes
Prime numbers
Nat.exists_infinite_primes3-stage walkthroughIrrationality of the Square Root of Two
Irrationality of radicals
irrational_sqrt_twoLagrange's Four-Square Theorem
Additive number theory
Nat.sum_four_squares5-stage walkthroughMöbius Inversion
Arithmetic functions and inversion
ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eqOstrowski's Theorem
Absolute values and places
Rat.AbsoluteValue.equiv_real_or_padicPell Equation Solvability
Diophantine equations
Pell.exists_iff_not_isSquareQuadratic Reciprocity
Quadratic residues
legendreSym.quadratic_reciprocity4-stage walkthroughWilson's Theorem
Prime congruences
Nat.prime_iff_fac_equiv_neg_one
Geometry & linear algebra
13 theoremsCarathéodory's Convex Hull Theorem
Convex geometry
convexHull_eq_unionCauchy–Schwarz Inequality
Inner-product geometry
norm_inner_le_normCayley–Hamilton Theorem
Characteristic polynomials
LinearMap.aeval_self_charpolyFinite-Dimensional Spectral Theorem
Spectral theory
LinearMap.IsSymmetric.diagonalization_apply_self_applyHelly’s Theorem
Convex geometry
Convex.helly_theoremHilbert’s Nullstellensatz
Affine algebraic geometry
MvPolynomial.vanishingIdeal_zeroLocus_eq_radicalLaw of Cosines
Euclidean affine geometry
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angleLaw of Sines
Euclidean affine geometry
EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_distPtolemy’s Theorem
Cyclic and cospherical geometry
EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cosphericalPythagorean Theorem
Inner-product geometry
norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zeroRadon's Theorem
Convex geometry
Convex.radon_partitionRank–Nullity Theorem
Linear maps and dimension
LinearMap.rank_range_add_rank_kerThales’ Theorem
Euclidean sphere geometry
EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter
Topology
9 theoremsArzelà–Ascoli Theorem
Compactness of function families
BoundedContinuousFunction.arzela_ascoliBaire Category Theorem
Baire spaces and category
dense_sInter_of_isOpenHeine–Borel Theorem
Metric topology
Metric.isCompact_iff_isClosed_boundedHeine–Cantor Theorem
Compactness and uniform spaces
CompactSpace.uniformContinuous_of_continuousIntermediate Value Theorem
Continuous interval maps
intermediate_value_IccStone–Weierstrass Theorem
Uniform approximation
ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints4-stage walkthroughTietze Extension Theorem — Bounded Real-Valued Form
Extension theorems
BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbeddingTychonoff's Theorem
Compactness
isCompact_pi_infinite3-stage walkthroughUrysohn's Lemma
Separation theorems
exists_continuous_zero_one_of_isClosed
Combinatorics
16 theoremsBirkhoff–von Neumann Theorem
Doubly stochastic matrices
doublyStochastic_eq_convexHull_permMatrixCauchy–Davenport Theorem
Additive combinatorics
ZMod.cauchy_davenportErdős–Ginzburg–Ziv Theorem
Additive combinatorics and zero-sum theory
ZMod.erdos_ginzburg_zivErdős–Ko–Rado Theorem
Extremal set theory
Finset.erdos_ko_radoEuler’s Odd–Distinct Partition Theorem
Enumerative partition theory
Nat.Partition.card_odds_eq_card_distinctsHales–Jewett Theorem
Ramsey theory
Combinatorics.Line.exists_mono_in_high_dimensionHall's Marriage Theorem
Matchings and systems of representatives
Finset.all_card_le_biUnion_card_iff_exists_injective5-stage walkthroughHandshaking Lemma
Finite graph invariants
SimpleGraph.even_card_odd_degree_verticesInclusion–Exclusion Principle
Enumerative combinatorics
Finset.inclusion_exclusion_card_biUnionKruskal–Katona Theorem
Extremal set theory
Finset.kruskal_katonaPigeonhole Principle
Finite combinatorics
Fintype.exists_ne_map_eq_of_card_ltRoth’s Theorem
Additive combinatorics
rothNumberNat_isLittleO_idSperner’s Theorem
Extremal set theory
IsAntichain.spernerSzemerédi’s Regularity Lemma
Graph regularity
szemeredi_regularityTurán’s Theorem
Extremal graph theory
SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraphTutte’s Perfect-Matching Theorem
Matching theory
SimpleGraph.tutte
Logic & computation
11 theoremsCantor's Theorem
Diagonal arguments
Function.cantor_surjective2-stage walkthroughCompactness Theorem for First-Order Logic
Models and compactness
FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiableDownward Löwenheim–Skolem Theorem
Elementary submodels and cardinality
FirstOrder.Language.exists_elementarySubstructure_card_eqŁoś's Theorem
Ultraproducts and transfer
FirstOrder.Language.Ultraproduct.sentence_realizeMyhill–Nerode Theorem
Formal languages and automata
Language.isRegular_iff_finite_range_leftQuotientRice's Theorem
Semantic properties of programs
ComputablePred.riceSchröder–Bernstein Theorem
Cardinality and bijections
Function.Embedding.schroeder_bernstein5-stage walkthroughUncountability of the Continuum
Cardinality and the continuum
Cardinal.not_countable_realUndecidability of the Halting Problem
Undecidability
ComputablePred.halting_problem2-stage walkthroughWell-Ordering Theorem
Choice and well-ordering
exists_wellOrderZorn’s Lemma
Maximality principles
zorn_le
Categories & order
4 theoremsFreyd–Mitchell Embedding Theorem
Abelian categories and exact embeddings
CategoryTheory.Abelian.freyd_mitchellJordan–Hölder Theorem
Composition series
CompositionSeries.jordan_holderKnaster–Tarski Theorem
Order-theoretic fixed-point theory
fixedPoints.completeLatticeYoneda Lemma
Representable functors
CategoryTheory.yonedaEquiv
Source and evidence
Mathlib supplies the theorems; ProofAtlas explains and rechecks them
Each page links to the exact upstream declaration and keeps the local Lean replay separate from the original theorem.
Audience
Who this collection is for
Mathematicians, students, formalizers, and curious readers who want a precise route from a familiar theorem to its exact Lean statement.
Editorial selection
Why these declarations
- The result is widely recognized as a landmark within a major area of mathematics.
- The selected declaration states the mathematical result directly rather than through a local wrapper.
- The collection spans major areas and favors results whose exact formal scope can be explained faithfully.
- The page can separate upstream mathematics, local replay evidence, explanatory media, and ProofAtlas publication status without ambiguity.