Public Mathlib landmark · existing upstream theorem · read-only
ProofAtlas

A curated map of major formalized mathematics

Landmark Theorems in Mathlib

Eight landmark results, indexed at exact Mathlib declarations and pinned source bytes. Each page separates the upstream theorem, a fresh local Lean evidence run, editorial review, and Proof Atlas acceptance.

Theorems
8
Source posture
Pinned upstream references
Visibility
Publicly indexed
An engraved mathematical landscape joins eight motifs: a complex root, equal coset clusters, signed area, prime beacons, reciprocal residue circles, a matching, a compact product, and a bijection.
Eight landmark formalizations form one navigable atlas, while every theorem page remains bound to its own exact upstream statement and evidence. Generated explanation only; the exact HTML statement and pinned source are authoritative.
Detailed visual description

On a dark forest-green engraved field, eight mathematical motifs are connected by fine gold paths: polynomial roots, repeated group clusters, calculus accumulation, an unending prime trail, quadratic-residue reciprocity, a bipartite matching, product compactness, and opposing injections resolved into a pairing.

Theorem families

Explore 8 landmark statements

A smooth curve spans two endpoints above layered blue and green signed accumulation, ending at one vertical endpoint difference.

Differentiation and integration · Analysis

Fundamental Theorem of Calculus

Under differentiability and integrability hypotheses, the oriented interval integral of a derivative equals the endpoint difference.

Upstream
intervalIntegral.integral_deriv_eq_sub
Evidence
Exact upstream declaration replayed
Six emerald vertices and six ivory vertices are paired row by row by six gold edges, with faint alternative bipartite edges and nested neighborhood contours.

Matchings and systems of representatives · Combinatorics

Hall's Marriage Theorem

A family of finite sets has distinct representatives exactly when every finite subfamily has a union at least as large as the subfamily.

Upstream
Finset.all_card_le_biUnion_card_iff_exists_injective
Evidence
Exact upstream declaration replayed
Opposing one-to-one arrows between emerald and cobalt nodes are reorganized into alternating chains and loops, then into a complete row-by-row pairing.

Cardinality and bijections · Set theory

Schröder–Bernstein Theorem

Injections in both directions between two types imply a bijection between them.

Upstream
Function.Embedding.schroeder_bernstein
Evidence
Exact upstream declaration replayed
A many-sheeted ivory polynomial surface narrows toward one luminous gold point on an abstract complex plane.

Polynomials · Algebra and complex analysis

Fundamental Theorem of Algebra

Every complex polynomial of positive degree has a complex root.

Upstream
Complex.exists_root
Evidence
Exact upstream declaration replayed
Emerald and cobalt residue circles exchange two gold arrows, with aligned and parity-reversed echoes below.

Quadratic residues · Number theory

Quadratic Reciprocity

For distinct odd primes, the two Legendre symbols are related by the quadratic-reciprocity sign.

Upstream
legendreSym.quadratic_reciprocity
Evidence
Exact upstream declaration replayed
A stone path passes a gate and continues toward an open horizon, marked by isolated gold beacons among irregular composite piles.

Prime numbers · Number theory

Infinitely Many Primes

For every natural-number threshold, there is a prime at or above it.

Upstream
Nat.exists_infinite_primes
Evidence
Exact upstream declaration replayed
An infinite field of enclosed coordinate worlds recedes into the distance while emerald and cobalt threads gather their chosen points into one luminous, enclosed product space.

Compactness · Topology

Tychonoff's Theorem

An arbitrary product of compact subsets is compact in the product topology.

Upstream
isCompact_pi_infinite
Evidence
Exact upstream declaration replayed
One emerald subgroup cluster is surrounded by seven congruent cobalt clusters that tile a larger circular group.

Subgroups and cardinality · Group theory

Lagrange's Theorem

The natural-number cardinality of a subgroup divides that of its ambient group.

Upstream
Subgroup.card_subgroup_dvd_card
Evidence
Exact upstream declaration replayed

Scope

Famous formal statements, already upstream

This collection is an editorial index into exact Mathlib declarations and selected local evidence. Proof Atlas does not claim to have discovered these theorems, authored the upstream source, or created a new result by replaying an existing declaration.

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