WikiLean

WikiLean

Wikipedia's mathematics, annotated with its formalization status in Mathlib.

A mirror of WikiProject Mathematics articles with every definition, theorem, and proof linked to its Lean formalization where one exists. A project by Jack McCarthy.

778articles
37,936annotated results
28%formalized
14%partial

4 not yet tagged · 3 awaiting count backfill

Recently updated

Datasets & graphs

All articles

formalized partial not formalized
029/46 110/20 1003/21 1000 (number)0/106 1729 (number)0/12 27/14 33/18 42/17 50/30 61/26 71/25 80/19 92/13 Abacus0/20 Abel Prizeuntagged Abelian category21/42 Abelian group39/60 Abelian variety2/43 Absolute value32/52 Abstract algebra19/32 Abstraction0/3 Accuracy and precision1/35 Action (physics)0/35 Actuarial science0/5 Addition51/79 Adjoint functors44/64 Adjoint representation8/33 Affine geometry6/25 Affine space43/100 Akaike information criterion1/22 Aleph number17/27 Algebra33/67 Algebra over a field33/51 Algebraic curve4/86 Algebraic geometry16/68 Algebraic K-theory1/102 Algebraic number19/33 Algebraic number field68/95 Algebraic number theory32/56 Algebraic structure31/43 Algebraic topology11/27 Algebraic variety6/54 Algebraically closed field31/63 Algorithm4/56 Almagest0/120 Altitude (triangle)4/26 American Mathematics Competitions0/7 Analog computer0/18 Analysis of algorithms1/18 Analytic function25/48 Analytic geometry9/41 Analytic number theory15/38 Ancient Greek mathematics9/34 Angle11/55 Applied mathematicsuntagged Arc length12/35 Archimedes Palimpsest0/9 Area11/62 Arithmetic42/92 Arithmetic function36/74 Arithmetic mean7/22 Arithmetical hierarchy1/50 Associative property11/28 Asymptotic analysis9/25 Atiyah–Singer index theorem2/38 Automorphic form1/9 Average1/25 Axiom4/37 Axiom of choice53/125 Axiom schema of replacement3/20 Ball (mathematics)18/32 Banach fixed-point theorem9/19 Banach space64/171 Banach–Tarski paradox3/50 Basis (linear algebra)37/50 Bayes' theorem12/29 Bayesian inference7/46 Bayesian probability1/10 Bell's theorem4/56 Bernoulli process11/44 Bézier curve6/51 Big O notation29/56 Bijection20/36 Bijection, injection and surjection22/24 Binary number6/57 Binary search tree0/24 Binary tree10/43 Binomial distribution7/55 Binomial series13/21 Birthday problem0/52 Block design1/63 Boolean algebra (structure)27/53 Borel–Kolmogorov paradox0/22 Borel–Weil–Bott theorem0/18 Boundary value problem0/15 Box–Muller transform0/20 Brouwer fixed-point theorem1/31 Butterfly effect0/12 C*-algebra17/45 Calculus of variations0/47 Cantor's diagonal argument9/22 Cantor's theorem12/16 Cardinal number64/90 Cardinality84/131 Cardinality of the continuum20/33 Cartan connection0/32 Cartesian coordinate system23/61 Category (mathematics)58/69 Category theory10/10 Catenary0/35 Cauchy sequence14/36 Cauchy–Schwarz inequality30/35 Cauchy's integral formula9/20 Cayley–Hamilton theorem11/42 Cellular automaton1/77 Center squeeze0/21 Central limit theorem20/53 Centroid6/47 Chain rule20/33 Chaos theory2/54 Character theory5/41 Characteristic class0/16 Characterizations of the exponential function5/34 Chebyshev polynomials25/70 Chebyshev's inequality7/50 Chern class0/59 Chi-squared distribution0/43 Chinese remainder theorem17/30 Church–Turing thesis3/31 Circle32/100 Circular motion1/39 Classical mechanics0/32 Classical orthogonal polynomials5/66 Classification of finite simple groups2/36 Clifford algebra37/101 Closed graph theorem (functional analysis)6/29 Cofinality19/37 Cohomology6/43 Coin flipping1/11 Combination18/30 Combinatorial design2/55 Combinatorial game theory0/35 Combinatorics13/55 Combinatory logic0/43 Common logarithm3/11 Commutative algebra10/12 Commutative diagram5/18 Commutative property11/20 Commutative ring82/115 Compact group5/29 Compact operator14/47 Compact space52/81 Complete graph4/24 Complete metric space42/57 Complex analysis15/22 Complex conjugate18/24 Complex number48/74 Complex plane14/41 Computable function13/34 Computational complexity theory5/73 Computer algebra system14/43 Concrete category9/23 Conditional expectation26/40 Conditional probability8/26 Confidence interval0/9 Conjecture2/33 Conjugacy class18/32 Connected space44/77 Constructible universe0/48 Context-free grammar15/75 Continuous function89/115 Continuum hypothesis13/33 Control theory0/41 Convergence of random variables25/46 Convex set36/70 Convolution26/85 Conway's Game of Life0/52 Cook–Levin theorem0/16 Coordinate system6/42 Coprime integers18/39 Copula (statistics)0/28 Correlation4/44 Cotangent space2/22 Countable set47/57 Covariance9/30 Covariance and contravariance of vectors25/54 Covariant derivative8/48 Covering space13/88 Coxeter group7/39 Cross product17/50 Cryptography0/64 Cube3/80 Cubic equation7/48 Curl (mathematics)2/57 Curry–Howard correspondence3/34 Curvature0/96 Curvature of Riemannian manifolds0/22 Curve6/49 Cyclic group29/55 Data structure0/13 De Moivre's formula7/21 Decision theory2/18 Derivative34/53 Determinant60/101 Diffeomorphism12/59 Difference engine5/18 Differentiable manifold21/61 Differential calculus16/27 Differential equation1/32 Differential form10/61 Differential geometry3/35 Differential geometry of surfaces6/133 Differential operator6/30 Diophantine approximation4/38 Dirac delta function14/91 Dirac equation1/75 Directed acyclic graph2/52 Discrete calculus22/69 Discrete Fourier transform7/48 Discrete mathematics1/28 Distance12/27 Distribution (mathematical analysis)27/75 Distributive property29/37 Divergence theorem0/16 Divergent series4/64 Division (mathematics)26/52 Division by zero14/40 Divisor30/41 Dot product24/43 Dual space34/69 Duality (mathematics)49/106 Dynamic programming1/55 Dynamical system31/112 E (mathematical constant)20/64 Eigenvalues and eigenvectors43/95 Elementary algebra14/56 Ellipse0/92 Elliptic curve23/87 Elliptic function6/14 Elliptic geometry1/45 Elliptic integral0/49 Empty set16/21 Entropy0/54 Entropy (information theory)4/30 Equality (mathematics)39/62 Equation solving5/31 Equivalence class20/27 Equivalence relation30/60 Erdős number0/36 Ergodic theory4/27 Erlangen program0/18 Étale cohomology3/26 Euclid's Elements22/49 Euclidean algorithm43/96 Euclidean distance15/33 Euclidean geometry25/51 Euclidean group0/26 Euclidean planes in three-dimensional space1/35 Euclidean space54/84 Euclidean vector23/50 Euler angles2/103 Euler characteristic2/41 Euler's constant3/54 Euler's formula30/39 Euler's identity11/16 Euler's theorem3/6 Euler's totient function13/48 Expected value29/40 Experimental mathematics0/24 Exponential distribution5/82 Exponential function29/58 Exponential growth1/24 Exponentiation74/114 Exterior algebra21/75 Factorial36/61 Fast Fourier transform1/28 Fermat's Last Theorem17/71 Fermat's little theorem6/17 Fiber bundle11/46 Fibonacci sequence17/75 Fibred category10/44 Field (mathematics)83/112 Field extension48/56 Fields Medal0/1 Finitary relation8/28 Finite difference22/55 Finite field34/63 Finite group14/24 First-order logic29/96 Five lemma6/8 Flat module24/49 Floor and ceiling functions22/70 Fluid mechanics0/33 Formal language11/27 Formal power series42/82 Formula3/10 Four color theorem2/49 Fourier analysis11/28 Fourier series11/36 Fourier transform30/79 Fractal5/40 Fractal dimension1/16 Frame bundle0/34 Fubini's theorem14/33 Function (mathematics)66/95 Functional analysis16/19 Functor34/43 Fundamental group19/76 Fundamental theorem of algebra13/34 Fundamental theorem of arithmetic17/29 Fundamental theorem of calculus7/14 Galois theory30/44 Game theory1/61 Gamma distribution5/95 Gamma function34/96 Gauss–Bonnet theorem0/22 Gaussian elimination2/34 General linear group19/47 General relativity0/62 General topology90/111 Generalized hypergeometric function14/88 Generalized Riemann hypothesis5/37 Generalized Stokes theorem3/20 Genus (mathematics)0/29 Geodesic2/56 Geometric group theory8/54 Geometric progression7/33 Geometric series11/25 Geometry10/43 Gibbs phenomenon0/24 Gödel numbering2/10 Gödel's incompleteness theorems7/80 Goldbach's conjecture2/45 Golden ratio7/52 Gradient8/45 Graph (discrete mathematics)28/53 Graph coloring13/157 Graph drawing0/38 Graph minor0/55 Graph of a function5/8 Graph theory30/138 Greatest common divisor33/58 Group (mathematics)54/66 Group action45/82 Group representation32/45 Haar measure13/43 Hahn–Banach theorem9/57 Hairy ball theorem0/12 Ham sandwich theorem0/17 Hamiltonian mechanics0/38 Harmonic analysis1/15 Harmonic function7/30 Hausdorff dimension11/31 Hausdorff space26/39 Hearing the shape of a drum2/46 Hexadecimal1/58 Hexagon0/39 Heyting algebra23/66 Hilbert space102/142 Hilbert's problems2/16 History of algebra24/67 History of geometry1/26 History of mathematical notation6/47 History of mathematics39/111 History of the function concept13/59 Hodge star operator2/56 Hölder's inequality17/34 Holonomy0/37 Hom functor17/20 Homeomorphism4/20 Homogeneous space7/32 Homological algebra26/32 Homology (mathematics)21/51 Homomorphism38/58 Homotopy18/57 Homotopy group4/19 Hopf algebra9/47 Hyperbola0/92 Hyperbolic functions33/67 Hyperbolic geometry4/231 Hypercomplex number4/37 Identity function11/15 Imaginary unit16/43 Improper integral7/34 Indian mathematics29/61 Information theory4/33 Inner product space44/56 Integer25/48 Integer factorization4/33 Integral35/80 Interpolation5/41 Interval (mathematics)32/61 Introduction to gauge theory4/30 Introduction to general relativity0/36 Intuitionistic logic15/69 Invariant theory1/19 Inverse trigonometric functions15/43 Inversive geometry20/131 Invertible matrix22/53 Isomorphism30/49 Isomorphism theorems14/24 Jordan normal form17/67 Kalman filter0/73 Karnaugh map0/34 Kepler's laws of planetary motion0/55 Kerala school of astronomy and mathematics5/9 Kinematics2/71 Kinetic energy0/33 Klein bottle0/28 Klein four-group12/36 Knot theory0/53 Kronecker delta7/35 Krull dimension21/43 Kullback–Leibler divergence4/27 Kurtosis0/34 L'Hôpital's rule4/26 Lagrange multiplier4/30 Lagrange's theorem (group theory)13/24 Lambert W function0/73 Langlands program0/26 Laplace operator12/73 Laplace transform1/54 Laplace's equation7/56 Latitude0/33 Lattice (group)10/31 Lattice (order)35/61 Law of cosines14/48 Law of large numbers3/19 Law of sines2/23 Least common multiple16/34 Least squares1/33 Lebesgue integral25/31 Lebesgue measure36/58 Lie algebra58/109 Lie group17/70 Likelihood-ratio test0/11 Limit (mathematics)48/63 Limit inferior and limit superior27/51 Limit of a function39/66 Lindemann–Weierstrass theorem0/17 Linear algebra50/67 Linear equation1/25 Linear map51/82 Linear programming2/59 Linear regression3/57 Linearity4/11 Liouville number13/23 Local ring19/40 Locally convex topological vector space40/92 Logarithm41/80 Logic3/88 Logical conjunction12/21 Logistic function7/60 Löwenheim–Skolem theorem10/17 Lp space47/107 Machine learning4/72 Magic square2/70 Magma (algebra)20/51 Map projection2/51 Margin of error0/28 Markov chain6/78 Martingale (probability theory)19/49 Mathcountsuntagged Mathematical analysis31/65 Mathematical constant23/48 Mathematical induction11/30 Mathematical logic15/83 Mathematical model6/58 Mathematical optimization10/67 Mathematical physics6/22 Mathematical proof6/25 Mathematician0/3 Mathematics21/79 Matrix (mathematics)60/105 Matrix multiplication25/41 Maximal ideal21/37 Maximum and minimum14/23 Maximum likelihood estimation1/67 Maxwell's equations2/65 Mean6/25 Mean value theorem19/28 Measurable function9/19 Median1/71 Metric space77/131 Metric tensor15/56 Minkowski space3/74 Minor (linear algebra)3/27 Möbius function10/31 Möbius strip0/66 Möbius transformation11/102 Model theory32/112 Modular arithmetic32/51 Module (mathematics)35/48 Monodromy4/24 Monoid42/66 Monte Carlo method1/23 Morphism27/34 Motive (algebraic geometry)0/37 Multiplication42/58 Naive set theory31/47 Nash equilibrium0/66 Natural logarithm21/37 Natural number48/61 Navier–Stokes equations0/82 Negative number28/37 Newton's method4/76 Nicolas Bourbaki4/7 Nilpotent group12/22 Non-Euclidean geometry5/56 Nondeterministic finite automaton23/38 Nonlinear programmingpending Norm (mathematics)30/49 Normal distribution20/138 Normal number0/47 NP-completeness1/27 NP-hardness0/18 Number52/80 Number theory46/77 Numerical analysis2/29 Numerical digit2/19 Numerical integration2/33 Numerical methods for ordinary differential equations1/46 Numerical stability0/13 Nyquist–Shannon sampling theorem0/27 On-Line Encyclopedia of Integer Sequences2/15 Open set14/39 Operator (mathematics)13/26 Order of magnitude0/25 Ordinal number55/85 Ordinary differential equation5/29 Orientability0/50 Orthogonal group19/109 Orthogonal matrix12/68 Orthogonality4/20 Outer product11/24 P versus NP problem2/62 P-adic number34/89 Parabola1/101 Parallel postulate0/18 Parameter5/37 Pareto distribution2/47 Parity (mathematics)14/37 Partial differential equation2/35 Partial function6/32 Partition of a set11/24 Pauli matrices0/79 Pell number0/6 Pentagon0/36 Pentagram2/28 Percentage0/24 Perfect graph9/83 Perfect number10/57 Periodic function20/29 Permutation40/99 Perturbation theory (quantum mechanics)13/85 Physics0/57 Pi30/86 Picard–Lindelöf theorem9/18 Pigeonhole principle18/34 Planar graph0/67 Platonic solid0/64 Point (geometry)9/22 Poisson distribution6/84 Poisson manifold0/111 Polygon5/56 Polynomial62/96 Polynomial interpolation12/33 Polytope0/33 Power law1/44 Power series32/52 Presentation of a group5/31 Prime ideal38/77 Prime number44/89 Primitive recursive function49/95 Principal component analysis1/34 Prisoner's dilemma0/49 Probability16/30 Probability density function14/37 Probability interpretations2/17 Probability space33/46 Probability theory31/48 Product (mathematics)24/29 Product rule11/28 Projective geometry6/28 Projective module21/49 Projective plane8/64 Projective space14/60 Proof that 22/7 exceeds π1/16 Proof theory1/26 Propositional calculus0/73 Propositional logic15/115 Pullback (differential geometry)5/18 Pure mathematics13/32 Putnam Competitionuntagged Pythagorean theorem22/55 Pythagorean triple13/108 Quadratic equation13/71 Quadratic form33/67 Quadratic formula3/17 Quadratic function6/45 Quadratic reciprocity29/66 Quadratic sievepending Quadrilateral2/127 Quantum chromodynamics0/37 Quantum computing2/68 Quantum electrodynamics0/42 Quantum field theory0/60 Quantum mechanics0/63 Quasigroup0/59 Quaternion32/78 Radian3/20 Ramsey's theorem1/94 Random variable24/50 Random walk1/56 Randomness0/21 Rank–nullity theorem8/25 Rate of convergence15/114 Ratio7/39 Rational function16/34 Real analysis85/106 Real projective line8/23 Real projective space0/29 Rectangle0/39 Recurrence relation12/45 Reflexive space6/66 Register machine4/35 Regression toward the mean1/18 Regular language2/33 Regular polytope0/52 Repeating decimal4/79 Representation theory24/34 Representation theory of finite groups33/122 Ricci calculus11/58 Riemann hypothesis20/134 Riemann integral0/30 Riemann sphere5/35 Riemann surface2/63 Riemann zeta function21/90 Riemannian manifold20/99 Riesz representation theorempending Ring (mathematics)97/148 Ring theory22/50 Roman numerals0/55 Root system22/95 Rotation0/20 Sampling (statistics)3/77 Scalar field theory0/50 Scalar multiplication27/41 Schrödinger equation2/59 Schwarzian derivative0/59 Scientific notation0/33 Second-order logic2/62 Self-adjoint operator20/75 Separable space16/42 Separation axiom30/59 Sequence59/87 Sequent calculus0/64 Set (mathematics)54/69 Set theory26/44 Seven Bridges of Königsberg10/20 Sheaf (mathematics)26/50 Shor's algorithm3/36 Signal processing1/18 Significant figures2/56 Simple continued fraction15/79 Simplex19/79 Simplex algorithm0/36 Simply typed lambda calculus0/55 Simpson's paradox0/18 Simulated annealing0/53 Singular value decomposition23/111 Slide rule5/33 Sobolev space2/39 Solvable group12/38 Spacetime3/80 Special unitary group4/57 Spectral sequence8/38 Spectral theorem12/35 Spectral theory10/15 Sphere13/68 Sphere packing2/38 Spherical coordinate system1/57 Spherical harmonics2/63 Split-complex number0/47 Square4/74 Square root21/40 Square root of 212/45 Squaring the circle6/43 Standard deviation5/62 Standard Model0/31 Standard probability space4/39 Stationary point6/24 Statistical hypothesis test2/52 Statistical mechanics0/12 Statistical significance0/16 Statistics3/72 Stereographic projection10/50 Stirling number4/28 Stochastic0/5 Stochastic process8/62 Stone–Weierstrass theorem15/27 Straightedge and compass construction0/52 String theory8/93 Structure (mathematical logic)23/49 Student's t-distribution0/53 Student's t-test4/72 Sturm–Liouville theory1/31 Subset21/32 Subtraction7/27 Surface (topology)4/64 Surjective function18/29 Sylow theorems26/38 Symmetric group54/99 Symmetry4/23 Symmetry (geometry)2/40 Symmetry in mathematics22/46 Synthetic geometry0/15 System F0/31 System of linear equations9/46 Tangent8/36 Tangent bundle12/40 Tangent space12/28 Taylor series20/51 Taylor's theorem25/40 Tensor13/55 Tensor product35/61 Tessellation1/69 Tesseract0/36 Tetrahedron7/66 Theorem6/33 Theoretical computer science0/31 Theory of relativity0/25 Theta function14/87 Time complexity5/63 Timeline of mathematics45/146 Topological group30/96 Topological space30/42 Topology21/43 Torus4/81 Total order38/50 Transcendental number16/92 Transcendental number theory4/42 Transfinite induction6/7 Trapezoid1/47 Travelling salesman problem0/69 Tree (graph theory)10/43 Triangle40/108 Triangle inequality29/47 Trigonometric functions27/61 Trigonometry12/19 Tuple11/22 Turing machine5/48 Type I and type II errors0/31 Type theory2/97 Uniform continuity20/36 Uniform convergence34/44 Unitary matrix7/16 Universal enveloping algebra8/45 Variance13/63 Vector bundle19/50 Vector calculus7/26 Vector field13/57 Vector space61/70 Velocity0/42 Von Neumann algebra4/113 Wave1/72 Wave equation0/32 Wavelet12/82 Weil conjectures0/15 Well-order27/49 Winding number1/36 Yang–Mills theory0/31 YBC 72890/7 Yuktibhāṣā7/11 Z-transform0/32 Zermelo–Fraenkel set theory15/40 Zeros and poles7/25 Zorn's lemma54/77