Browse by theorem
Formalizations
A formalization translates a mathematical claim into a precise statement and proof that Lean checks step by step. Browse results by subject, with visual intuition, exact statements, and complete source.
Featured mathematics
Natural-Density Collatz Descent in Logarithmic Time
Question: If a threshold tends to infinity—however slowly—how quickly do almost all Collatz starts fall below it?
Proof routePhase gap→Syracuse control→Raw-time lift
Boundary: Density one may leave a density-zero exceptional set. This does not prove convergence for every start or arrival at 1.
Published evidence
More public formalizations
Collatz Predecessor Lower Bounds at Exponent 0.90
3 theorem variantsThree eventual forms for each fixed positive target not divisible by 3.
Three accepted exact predecessor-count lower bounds remain available as a separate theorem family.
3 recorded declarations58 first-party Lean files · 10,237 lines
Geometry & topology
7 formalizationsEuclidean geometry
Butterfly Theorem
In the checked nondegenerate butterfly configuration, the opposite-chord intersections X and Y have the original chord midpoint M as their midpoint.
2 recorded declarations1 first-party Lean file · 3,197 lines
Published formalization
Public evidence page
Incidence geometry
Sylvester–Gallai Theorem
A finite set of more than two points in ℝ² that is not all on one line has a pair whose line contains no third point of the set.
3 recorded declarations1 first-party Lean file · 1,625 lines
Published formalization
Public evidence page
Lattice geometry
Algebraic Lemma Toward Pick’s Theorem
For any finite cyclic list of lattice vertices inside a coordinate box, its signed shoelace-area sum equals the associated weighted lattice-point sum.
3 recorded declarations1 first-party Lean file · 1,203 lines
Published formalization
Public evidence page
Projective geometry
Brianchon’s Theorem
For six recorded nonzero tangent lines to a nonsingular real projective conic, the three joins of opposite consecutive-line intersections are concurrent.
3 recorded declarations2 first-party Lean files · 1,107 lines
Published formalization
Public evidence page
Topology
No Retraction from the Disk onto Its Boundary Circle
No continuous map from the closed complex unit disk to its boundary circle can fix every boundary point.
2 recorded declarations1 first-party Lean file · 233 lines
Published formalization
Public evidence page
Geometry
Heron’s Formula — Coordinate Identity
For any three points in ℝ², the square of twice their signed coordinate area equals four times the Heron radicand of their side lengths.
4 recorded declarations1 first-party Lean file · 86 lines
Published formalization
Public evidence page
Geometry
Napoleon’s Theorem — Algebraic Core
Given three complex points and ω² − ω + 1 = 0, the centroids of consistently oriented equilateral constructions on their sides form an equilateral triple.
4 recorded declarations1 first-party Lean file · 74 lines
Published formalization
Public evidence page
Discrete mathematics
9 formalizationsGraph theory
Brooks’s Theorem
Every finite connected simple graph that is neither complete nor an odd cycle can be vertex-colored using at most its maximum degree many colors.
1 recorded declaration1 first-party Lean file · 3,373 lines
Published formalization
Public evidence page
Graph theory · linear algebra
Kirchhoff’s Matrix-Tree Theorem
For any finite simple graph and chosen root, the determinant of the integer reduced Laplacian equals the number of spanning trees.
2 recorded declarations1 first-party Lean file · 2,043 lines
Published formalization
Public evidence page
Enumerative combinatorics
Hook-Length Formula
For every finite Young diagram, multiplying all hook lengths by the number of standard Young tableaux gives the factorial of the number of cells.
2 recorded declarations1 first-party Lean file · 3,692 lines
Published formalization
Public evidence page
Enumerative graph theory
Cayley’s Formula for Labeled Trees
For every n ≥ 1, the number of labeled unrooted trees on the vertex set Fin n is exactly n^(n − 2).
2 recorded declarations1 first-party Lean file · 2,756 lines
Published formalization
Public evidence page
Order theory
Dilworth’s Theorem
Every finite poset in which each antichain has at most k elements admits a cover of all elements by k chains.
2 recorded declarations1 first-party Lean file · 1,386 lines
Published formalization
Public evidence page
Graph theory
König’s Edge-Coloring Theorem
Every finite bipartite simple graph admits a proper edge coloring using its maximum degree many colors.
2 recorded declarations1 first-party Lean file · 1,070 lines
Published formalization
Public evidence page
Graph theory
Friendship Theorem
In a finite graph with at least two vertices, exactly one common neighbor for every distinct pair forces a universal hub; every other vertex has exactly one neighbor other than the hub.
3 recorded declarations1 first-party Lean file · 1,032 lines
Published formalization
Public evidence page
Partitions
Euler Pentagonal Recurrence
For every positive integer n, p(n) equals the exact finite alternating sum of earlier partition numbers at generalized pentagonal offsets 1, 2, 5, 7, ….
3 recorded declarations1 first-party Lean file · 698 lines
Published formalization
Public evidence page
Combinatorics
Erdős–Szekeres Monotone Subsequence Theorem
Any injective sequence of r · s + 1 values in a linear order contains either a strictly increasing subsequence of length r + 1 or a strictly decreasing one of length s + 1.
1 recorded declaration1 first-party Lean file · 251 lines
Published formalization
Public evidence page
Number theory & analysis
5 formalizationsNumber theory · dynamical systems
Tao’s Almost-Bounded Collatz Orbits
For every real-valued threshold function f on ℕ that tends to infinity, the positive starting values N whose standard Collatz orbit minimum is strictly below f(N) have logarithmic density one.
2 recorded declarations397 first-party Lean files · 124,019 lines
Published formalization
Public evidence page
Number theory · dynamical systems
Power-Saving Bound for Logarithmic-Time Collatz Descent
For every N ≥ 15,552, the proportion of natural numbers n < N that do not fall below their starting value within k ≤ log n accelerated Collatz steps is at most 10,000,000 · N⁻¹ᐟ¹⁰⁰.
1 recorded declaration20 first-party Lean files · 2,511 lines
Published formalization
Public evidence page
Number theory
Wolstenholme’s Theorem
For every prime p > 3, the sum 1 + 1/2 + ⋯ + 1/(p − 1), with reciprocals interpreted modulo p², is 0 modulo p².
2 recorded declarations1 first-party Lean file · 357 lines
Published formalization
Public evidence page
Diophantine approximation
Power-Law Phase Gap for Multiples of log₂ 3
There exists a positive constant c such that every positive integer q satisfies c · q⁻¹³³ᐟ¹⁰ ≤ ‖q log₂ 3‖, the distance to the nearest integer.
1 recorded declaration40 first-party Lean files · 8,926 lines
Published formalization
Public evidence page
Analysis
Fourier L¹/L² Compatibility Bridge
The function-level Fourier transform agrees almost everywhere with its L² representative for ℝ → ℂ functions in both L¹ and L².
3 recorded declarations1 first-party Lean file · 337 lines
Published formalization
Public evidence page
Line counts exclude blank lines; comments and documentation count. Totals cover each commit-pinned first-party Lean import closure and exclude Mathlib and other third-party dependencies.
Existing formal 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.
Exact status: These are existing upstream Mathlib declarations, not new ProofAtlas results. The pages bind pinned upstream source references to fresh local replay evidence, with reviewed public explanations and explicit acceptance boundaries.
- Landmarks
- 8
- Source
- Mathlib
- Atlas status
- Reviewed public index