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
Explicit Positive-Density Collatz Convergence in Logarithmic Time
Question: How many positive starts reach 1 within an explicit logarithmic number of ordinary Collatz steps?
For every natural X ≥ X₀, at least cX positive integers n < X reach 1 within 10.46 ln(n) ordinary Collatz steps, for fixed explicit c > 0 and X₀.
Each ordinary step sends an even n to n/2 and an odd n to 3n+1; ln is the natural logarithm. The 10.48 corollary uses the same density constant and cutoff.
Lean checks the exact public declarations, with a retained build transcript and clean-source collection record. The exact formal result is accepted in ProofAtlas.
Boundary: The guaranteed fraction is extremely small and the cutoff extremely large. The full Collatz conjecture remains open; this gives no density-one convergence, optimality, or historical-priority claim.
Public hosting does not accept the Lean result.
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
Featured formalizations
6 substantial proof destinationsStart with formalizations selected for mathematical significance, proof depth, and explanatory richness. The remaining catalog is organized by subject below.
Number 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
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
Graph theory
12-Vertex Hamilton Counterexample
Kernel-checked Lean proof that an explicit 12-vertex regular bipartite tournament has no Hamilton decomposition. The statement matches the unrestricted formulation recorded by Granet and Liebenau–Pehova.
1 recorded declaration6 first-party Lean files · 1,662 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
Euclidean 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
Geometry & topology
5 formalizationsLattice 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
8 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
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
Graph theory
Bondy's Minimum-Degree Longest-Cycle Conjecture
The companion paper presents a candidate proof of Bondy's minimum-degree longest-cycle conjecture. Paper-to-formal-statement alignment is under review. Lean checks only the exact displayed endpoint Bondy.bondy_longest_cycle at the audited source commit; its 204-module first-party cone reports only standard classical foundations.
1 recorded declaration204 first-party Lean files · 101,839 lines
Public Lean formalization · review pending
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
Natural-Density Collatz Descent in Logarithmic Time
For thresholds tending to infinity along odd inputs, odd-relative-density-one many odd starts descend within 145 · log N Syracuse steps; for thresholds tending to infinity on all positive inputs, ordinary-natural-density-one many positive starts descend within 436 · log N raw Collatz steps.
2 recorded declarations599 first-party Lean files · 182,625 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
More formalizations
2Complex analysis
Sendov's Conjecture
The submitted Lean package checks Sendov.sendov_conjecture: for a nonzero complex polynomial of degree at least two whose zeros lie in the closed unit disk, every zero lies within distance 1 of a critical point. Its relationship to the informal Sendov conjecture is not yet reviewed, and ProofAtlas accepted-result review remains pending.
1 recorded declaration1,160 first-party Lean files · 92,816 lines
Public Lean formalization · review pending
Public evidence page
Convex geometry
Moser's Convex Worm Mixed-Area Lower Bound
Four Lean-checked pointwise area inequalities cover finite polygonal worms and all unit worms, with direct motions or reflections allowed. Their strict rational corollaries give the lower bound 0.23743658226923856768; the exact optimum remains open.
8 recorded declarations72 first-party Lean files · 16,269 lines
Public Lean formalization · review pending
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
Explore landmark results at their exact Mathlib declarations and pinned source bytes. Each theorem page keeps the upstream result, a fresh local Lean evidence run, editorial review, and ProofAtlas publication status visibly distinct.
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
- 121
- Source
- Mathlib
- Atlas status
- Reviewed public index