Find formal mathematics
Search ProofAtlas
Search theorem titles, mathematical ideas, exact Lean declarations, and stable artifact identifiers. Results lead to one canonical theorem or formalization page instead of duplicating its source and review records.
Theorems and formalizations
46 canonical destinations · 23 ProofAtlas formalizations · 23 Mathlib landmarks
Collatz Predecessor Lower Bounds at Exponent 0.90
A standalone Lean 4 development proves that, for every fixed positive target not divisible by 3, the accelerated-Collatz predecessor count is eventually at least x^0.90, in both real- and natural-cutoff forms. A stronger target-dependent positive-constant x^0.901 bound supplies the exponent reserve. Lean checks the exact theorem chain; two disclosed native finite checks are independently replayed over 344,373,768 exact inequalities. This strengthens the retained Proof Atlas 0.88 result but does not prove the Collatz conjecture or provide an explicit eventual cutoff.
CollatzPredecessor090.predecessor_count_lower_bound_090CollatzPredecessor090.predecessor_count_lower_bound_090_natCollatzPredecessor090.predecessor_count_lower_bound_0901Open theorem page ProofAtlas formalizationEuclidean geometryButterfly Theorem
In the checked nondegenerate butterfly configuration, the opposite-chord intersections X and Y have the original chord midpoint M as their midpoint.
AtlasKnownTheorems.ButterflyTheorem.nondegenerateButterflyTheoremAtlasKnownTheorems.ButterflyTheorem.NondegenerateButterflyTheoremStatementOpen theorem page ProofAtlas formalizationIncidence geometrySylvester–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.
AtlasKnownTheorems.SylvesterGallai.sylvesterGallaiAtlasKnownTheorems.SylvesterGallai.sylvesterGallai_statementAtlasKnownTheorems.SylvesterGallai.SylvesterGallaiStatementOpen theorem page ProofAtlas formalizationLattice geometryAlgebraic 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.
AtlasKnownTheorems.PickLemma.algebraic_pick_lemmaAtlasKnownTheorems.PickLemma.AlgebraicPickLemmaAtlasKnownTheorems.PickLemma.algebraicPickLemma_of_edgeWeight_eqOpen theorem page ProofAtlas formalizationProjective geometryBrianchon’s Theorem
For six recorded nonzero tangent lines to a nonsingular real projective conic, the three joins of opposite consecutive-line intersections are concurrent.
AtlasKnownTheorems.BrianchonTheorem.brianchonTheoremAtlasKnownTheorems.BrianchonTheorem.BrianchonTheoremStatementAtlasKnownTheorems.BrianchonTheorem.brianchonTheoremStatement_v0_falseOpen theorem page ProofAtlas formalizationTopologyNo 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.
AtlasKnownTheorems.NoRetractionDiskCircle.noRetractionDiskCircleAtlasKnownTheorems.NoRetractionDiskCircle.NoRetractionDiskCircleStatementOpen theorem page ProofAtlas formalizationGeometryHeron’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.
AtlasKnownTheorems.HeronFormula.coordinate_heron_factor_identityAtlasKnownTheorems.HeronFormula.heron_factor_identityAtlasKnownTheorems.HeronFormula.heronFormulaOpen theorem page ProofAtlas formalizationGeometryNapoleon’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.
AtlasKnownTheorems.NapoleonTheorem.napoleon_centroid_relationAtlasKnownTheorems.NapoleonTheorem.napoleonTheoremAtlasKnownTheorems.NapoleonTheorem.napoleonTheorem_statementOpen theorem page ProofAtlas formalizationGraph theoryBrooks’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.
AtlasKnownTheorems.BrooksTheorem.brooksTheoremOpen theorem page ProofAtlas formalizationGraph theory · linear algebraKirchhoff’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.
AtlasKnownTheorems.MatrixTreeTheorem.matrixTreeTheoremAtlasKnownTheorems.MatrixTreeTheorem.MatrixTreeTheoremStatementOpen theorem page ProofAtlas formalizationEnumerative combinatoricsHook-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.
AtlasKnownTheorems.HookLengthFormula.hookLengthFormulaAtlasKnownTheorems.HookLengthFormula.HookLengthFormulaStatementOpen theorem page ProofAtlas formalizationEnumerative graph theoryCayley’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).
AtlasKnownTheorems.CayleyTreeFormula.cayleyTreeFormulaAtlasKnownTheorems.CayleyTreeFormula.CayleyTreeFormulaStatementOpen theorem page ProofAtlas formalizationOrder theoryDilworth’s Theorem
Every finite poset in which each antichain has at most k elements admits a cover of all elements by k chains.
AtlasKnownTheorems.DilworthTheorem.dilworthTheoremAtlasKnownTheorems.DilworthTheorem.DilworthTheoremStatementOpen theorem page ProofAtlas formalizationGraph theoryKönig’s Edge-Coloring Theorem
Every finite bipartite simple graph admits a proper edge coloring using its maximum degree many colors.
AtlasKnownTheorems.KonigEdgeColoringTheorem.KonigEdgeColoringStatementAtlasKnownTheorems.KonigEdgeColoringTheorem.konigEdgeColoringTheoremOpen theorem page ProofAtlas formalizationGraph theoryFriendship 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.
AtlasKnownTheorems.FriendshipTheorem.exists_hub_of_uniqueAtlasKnownTheorems.FriendshipTheorem.friendshipTheoremAtlasKnownTheorems.FriendshipTheorem.FriendshipTheoremStatementOpen theorem page ProofAtlas formalizationPartitionsEuler 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, ….
AtlasKnownTheorems.EulerPentagonal.euler_product_pentagonal_expansionAtlasKnownTheorems.EulerPentagonal.eulerPentagonalRecurrenceAtlasKnownTheorems.EulerPentagonal.EulerPentagonalRecurrenceOpen theorem page ProofAtlas formalizationCombinatoricsErdő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.
AtlasKnownTheorems.ErdosSzekeresMonotone.erdosSzekeresMonotoneOpen theorem page ProofAtlas formalizationNumber theory · dynamical systemsTao’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.
Erdos1135.Tao.taoAlmostBounded_checkedErdos1135.Tao.taoAlmostBoundedColMin_checkedOpen theorem page ProofAtlas formalizationNumber theory · dynamical systemsNatural-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.
Erdos1135.ND.ndRhinLogTimePaperPackageErdos1135.ND.ndRhinRawCollatzSqrtLogTimeBracketOpen theorem page ProofAtlas formalizationNumber theory · dynamical systemsPower-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⁻¹ᐟ¹⁰⁰.
Erdos1135.Terras.natCountingRatio_finiteStoppingTime_log_failure_le_powerOpen theorem page ProofAtlas formalizationNumber theoryWolstenholme’s Theorem
For every prime p > 3, the sum 1 + 1/2 + ⋯ + 1/(p − 1), with reciprocals interpreted modulo p², is 0 modulo p².
AtlasKnownTheorems.WolstenholmeTheorem.wolstenholmeTheoremAtlasKnownTheorems.WolstenholmeTheorem.WolstenholmeTheoremStatementOpen theorem page ProofAtlas formalizationDiophantine approximationPower-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.
Erdos1135.ND.existsPhaseGapRhinOpen theorem page ProofAtlas formalizationAnalysisFourier L¹/L² Compatibility Bridge
The function-level Fourier transform agrees almost everywhere with its L² representative for ℝ → ℂ functions in both L¹ and L².
AtlasKnownTheorems.FourierL1L2Compatibility.fourier_ae_eq_l2_fourier_of_memLp_one_twoAtlasKnownTheorems.FourierL1L2Compatibility.function_fourier_eLpNorm_eq_of_memLp_one_twoAtlasKnownTheorems.FourierL1L2Compatibility.function_fourier_l2_tempered_bridgeOpen theorem page Existing Mathlib theoremAnalysisBanach Fixed-Point Theorem
A contraction on a complete extended metric space has a fixed point reached by iterating from any chosen point with finite first displacement, together with an explicit geometric error bound.
ContractingWith.exists_fixedPointOpen theorem page Existing Mathlib theoremLogic and set theoryCantor's Theorem
No function from a type to its power set is surjective.
Function.cantor_surjectiveOpen theorem page Existing Mathlib theoremLinear algebra and analysisCauchy–Schwarz Inequality
The norm of an inner product is at most the product of the two vector norms.
norm_inner_le_normOpen theorem page Existing Mathlib theoremLinear algebraCayley–Hamilton Theorem
An endomorphism of a finite free module over a commutative ring annihilates its own characteristic polynomial.
LinearMap.aeval_self_charpolyOpen theorem page Existing Mathlib theoremProbability and analysisCentral Limit Theorem
Centered, unit-second-moment independent identically distributed real random variables have normalized sums converging in distribution to the standard Gaussian law.
ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sumOpen theorem page Existing Mathlib theoremNumber theory and algebraChinese Remainder Theorem
For coprime natural moduli m and n, residues modulo m*n form a ring equivalent to ordered pairs of residues modulo m and modulo n.
ZMod.chineseRemainderOpen theorem page Existing Mathlib theoremNumber theoryFermat's Little Theorem
If p is prime and n is coprime to p, then n^(p-1) is congruent to 1 modulo p.
Nat.ModEq.pow_card_sub_one_eq_oneOpen theorem page Existing Mathlib theoremAlgebra and complex analysisFundamental Theorem of Algebra
Every complex polynomial of positive degree has a complex root.
Complex.exists_rootOpen theorem page Existing Mathlib theoremNumber theoryFundamental Theorem of Arithmetic
Any finite list of primes whose product is n is a permutation of Mathlib's canonical prime-factor list for n.
Nat.primeFactorsList_uniqueOpen theorem page Existing Mathlib theoremAnalysisFundamental Theorem of Calculus
Under differentiability and integrability hypotheses, the oriented interval integral of a derivative equals the endpoint difference.
intervalIntegral.integral_deriv_eq_subOpen theorem page Existing Mathlib theoremCombinatoricsHall'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.
Finset.all_card_le_biUnion_card_iff_exists_injectiveOpen theorem page Existing Mathlib theoremNumber theoryInfinitely Many Primes
For every natural-number threshold, there is a prime at or above it.
Nat.exists_infinite_primesOpen theorem page Existing Mathlib theoremTopology and analysisIntermediate Value Theorem
A continuous function on a closed interval attains every value between its endpoint values in the selected increasing endpoint orientation.
intermediate_value_IccOpen theorem page Existing Mathlib theoremNumber theoryLagrange's Four-Square Theorem
Every natural number is a sum of four squares of natural numbers.
Nat.sum_four_squaresOpen theorem page Existing Mathlib theoremGroup theoryLagrange's Theorem
The natural-number cardinality of a subgroup divides that of its ambient group.
Subgroup.card_subgroup_dvd_cardOpen theorem page Existing Mathlib theoremCalculus and analysisMean Value Theorem
Some interior tangent to a differentiable real curve is parallel to the secant joining the interval endpoints.
exists_deriv_eq_slopeOpen theorem page Existing Mathlib theoremGeometry and linear algebraPythagorean Theorem
In a real inner-product space, the squared-norm identity for a vector sum holds exactly when the summands are orthogonal.
norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zeroOpen theorem page Existing Mathlib theoremNumber theoryQuadratic Reciprocity
For distinct odd primes, the two Legendre symbols are related by the quadratic-reciprocity sign.
legendreSym.quadratic_reciprocityOpen theorem page Existing Mathlib theoremLinear algebraRank–Nullity Theorem
For a linear map under Mathlib's rank-nullity hypothesis, the cardinal ranks of the range and kernel add to the rank of the domain.
LinearMap.rank_range_add_rank_kerOpen theorem page Existing Mathlib theoremSet theorySchröder–Bernstein Theorem
Injections in both directions between two types imply a bijection between them.
Function.Embedding.schroeder_bernsteinOpen theorem page Existing Mathlib theoremAnalysis and topologyStone–Weierstrass Theorem
A point-separating real subalgebra of continuous functions on a compact space is dense in the entire continuous-function algebra.
ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPointsOpen theorem page Existing Mathlib theoremTopologyTychonoff's Theorem
An arbitrary product of compact subsets is compact in the product topology.
isCompact_pi_infiniteOpen theorem page Existing Mathlib theoremComputability and logicUndecidability of the Halting Problem
For every fixed input, Mathlib's predicate that an encoded program is defined on that input is not computable.
ComputablePred.halting_problemOpen theorem page No matching theorem
Try a broader mathematical phrase
Search by a theorem name, subject, Lean declaration, or idea such as compactness, graph coloring, Fourier transform, or Collatz.