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.

764articles
34,532annotated results
27%formalized
14%partial

7 not yet tagged

Recently updated

Datasets & graphs

All articles

formalized partial not formalized
027/43 110/20 1003/18 1000 (number)0/84 1729 (number)0/10 27/14 33/18 42/17 50/30 61/26 71/22 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/31 Action (physics)0/27 Actuarial science0/5 Addition45/71 Adjoint functors43/63 Adjoint representation6/31 Affine geometry6/25 Affine space40/96 Akaike information criterion0/20 Aleph number17/27 Algebra33/67 Algebra over a field24/40 Algebraic curve4/86 Algebraic geometry16/68 Algebraic K-theory1/102 Algebraic number19/33 Algebraic number field50/77 Algebraic number theory32/56 Algebraic structure31/43 Algebraic topology11/27 Algebraic variety6/54 Algorithm1/50 Altitude (triangle)4/26 American Mathematics Competitions0/7 Analog computer0/18 Analysis of algorithms1/18 Analytic function25/48 Analytic geometry7/38 Analytic number theory15/38 Ancient Greek mathematics9/34 Angle11/55 Applied mathematicsuntagged Arc length8/29 Archimedes Palimpsest0/9 Area11/62 Arithmetic42/92 Arithmetic function36/74 Arithmetic mean7/22 Arithmetical hierarchy1/46 Associative property11/28 Asymptotic analysis9/25 Atiyah–Singer index theorem2/38 Automorphic form1/9 Average1/20 Axiom4/37 Axiom of choice53/125 Axiom schema of replacement3/20 Ball (mathematics)17/31 Banach fixed-point theorem9/19 Banach space61/167 Banach–Tarski paradox3/50 Basis (linear algebra)32/47 Bayes' theorem12/29 Bayesian inference7/46 Bayesian probability1/10 Bell's theorem3/35 Bernoulli process11/44 Bézier curve3/48 Big O notation29/56 Bijection20/36 Bijection, injection and surjection22/24 Binary number6/57 Binary search tree0/24 Binary tree9/42 Binomial distribution7/55 Binomial series13/21 Birthday problem0/49 Block design1/63 Boolean algebra (structure)25/44 Borel–Kolmogorov paradox0/22 Borel–Weil–Bott theorem0/18 Boundary value problem0/15 Box–Muller transform0/14 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 Cardinality77/123 Cardinality of the continuum14/25 Cartan connection0/32 Cartesian coordinate system21/57 Category (mathematics)47/57 Category theory10/10 Catenary0/35 Cauchy sequence14/36 Cauchy–Schwarz inequality21/27 Cauchy's integral formula7/18 Cayley–Hamilton theorem11/42 Cellular automaton1/64 Center squeeze0/21 Central limit theorem11/40 Centroid5/45 Chain rule20/33 Chaos theory1/44 Character theory5/41 Characteristic class0/13 Characterizations of the exponential function5/34 Chebyshev polynomials25/70 Chebyshev's inequality7/50 Chern class0/59 Chi-squared distribution0/39 Chinese remainder theorem17/30 Church–Turing thesis2/25 Circle32/100 Circular motion1/35 Classical mechanics0/32 Classical orthogonal polynomials5/66 Classification of finite simple groups2/36 Clifford algebra37/101 Closed graph theorem (functional analysis)5/27 Cofinality19/37 Cohomology6/43 Coin flipping1/11 Combination18/30 Combinatorial design2/55 Combinatorial game theory0/35 Combinatorics10/49 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 space41/56 Complex analysis15/22 Complex conjugate14/19 Complex number41/66 Complex plane14/41 Computable function13/34 Computational complexity theory4/60 Computer algebra system4/31 Concrete category9/23 Conditional expectation26/40 Conditional probability8/26 Confidence interval0/9 Conjecture2/33 Conjugacy class18/32 Connected space44/77 Constructible universe0/45 Context-free grammar14/70 Continuous function73/98 Continuum hypothesis6/24 Control theory0/41 Convergence of random variables28/49 Convex set36/67 Convolution26/85 Conway's Game of Life0/52 Cook–Levin theorem0/16 Coordinate system6/42 Coprime integers10/31 Copula (statistics)0/28 Correlation3/40 Cotangent space2/22 Countable set38/45 Covariance9/30 Covariance and contravariance of vectors23/50 Covariant derivative8/48 Covering space10/80 Coxeter group7/39 Cross product17/50 Cryptography0/52 Cube1/72 Cubic equation7/48 Curl (mathematics)2/43 Curry–Howard correspondence3/34 Curvature0/86 Curvature of Riemannian manifolds0/22 Curve6/49 Cyclic group29/55 Data structure0/13 De Moivre's formula7/21 Decision theory0/14 Derivative34/53 Determinant47/79 Diffeomorphism8/52 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 calculus18/60 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)17/38 Division by zero14/40 Divisor27/35 Dot product21/38 Dual space31/66 Duality (mathematics)untagged Dynamic programming0/52 Dynamical system18/90 E (mathematical constant)15/53 Eigenvalues and eigenvectors39/90 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 Elements16/40 Euclidean algorithm43/96 Euclidean distance15/33 Euclidean geometry20/40 Euclidean group0/26 Euclidean planes in three-dimensional space1/35 Euclidean space50/77 Euclidean vector23/50 Euler characteristic2/41 Euler's constant3/49 Euler's formula20/28 Euler's identity11/16 Euler's theorem3/6 Euler's totient function9/43 Expected value29/40 Experimental mathematics0/24 Exponential distribution5/74 Exponential function29/58 Exponential growth1/24 Exponentiation72/111 Exterior algebra21/75 Factorial36/61 Fast Fourier transform1/28 Fermat's Last Theorem14/61 Fermat's little theorem6/17 Fiber bundle11/46 Fibonacci sequence12/68 Fibred category10/44 Field (mathematics)76/100 Field extension41/49 Fields Medal0/1 Finitary relation6/25 Finite difference18/48 Finite field29/55 Finite group14/24 First-order logic28/95 Five lemma6/8 Flat module24/49 Floor and ceiling functions21/68 Fluid mechanics0/27 Formal language11/27 Formal power seriesuntagged Formula3/10 Four color theorem2/49 Fourier analysis11/28 Fourier series11/36 Fourier transform23/61 Fractal5/40 Fractal dimension1/16 Frame bundle0/34 Fubini's theorem12/28 Function (mathematics)61/89 Functional analysis10/12 Functor24/33 Fundamental group19/76 Fundamental theorem of algebra13/34 Fundamental theorem of arithmetic17/29 Fundamental theorem of calculus7/14 Galois theory15/29 Game theory1/61 Gamma distribution4/90 Gamma function33/93 Gauss–Bonnet theorem0/22 Gaussian elimination1/28 General linear group19/47 General relativity0/62 General topology90/111 Generalized hypergeometric function9/69 Generalized Riemann hypothesis5/36 Generalized Stokes theorem3/20 Genus (mathematics)0/28 Geodesic2/56 Geometric group theory7/34 Geometric progression6/30 Geometric series11/25 Geometry10/43 Gibbs phenomenon0/17 Gödel numbering2/10 Gödel's incompleteness theorems4/71 Goldbach's conjecture2/41 Golden ratio7/52 Gradient8/41 Graph (discrete mathematics)28/53 Graph coloring13/157 Graph drawing0/38 Graph minor0/52 Graph of a function5/8 Graph theory16/107 Greatest common divisor33/58 Group (mathematics)54/66 Group action43/80 Group representation17/27 Haar measure13/43 Hahn–Banach theorem11/50 Hairy ball theorem0/12 Ham sandwich theorem0/17 Hamiltonian mechanics0/38 Harmonic analysis1/15 Harmonic function7/30 Hausdorff dimension11/31 Hausdorff space26/39 Hexadecimal1/58 Hexagon0/39 Heyting algebra21/64 Hilbert space87/123 Hilbert's problems2/14 History of algebra15/56 History of geometry1/26 History of mathematical notation6/47 History of mathematics39/111 History of the function concept11/55 Hodge star operator1/50 Hölder's inequality14/30 Holonomy0/37 Hom functor17/20 Homeomorphism4/20 Homogeneous space7/32 Homological algebra21/26 Homology (mathematics)21/51 Homomorphism38/58 Homotopy15/44 Homotopy group4/19 Hopf algebra9/47 Hyperbola0/92 Hyperbolic functions30/60 Hypercomplex number4/37 Identity function11/15 Imaginary unituntagged Improper integral7/34 Indian mathematics27/58 Information theory4/33 Inner product space38/50 Integer25/48 Integer factorization3/29 Integral32/71 Interpolation4/35 Interval (mathematics)28/55 Introduction to gauge theory4/30 Introduction to general relativity0/36 Intuitionistic logic12/63 Invariant theory1/19 Inverse trigonometric functions10/37 Invertible matrix16/44 Isomorphism27/46 Isomorphism theorems13/22 Jordan normal form10/60 Kalman filter0/62 Karnaugh map0/26 Kepler's laws of planetary motion0/37 Kerala school of astronomy and mathematics5/9 Kinematics2/71 Kinetic energy0/33 Klein bottle0/28 Klein four-group5/27 Knot theory0/53 Kronecker delta7/34 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)9/29 Lattice (order)35/61 Law of cosines14/48 Law of large numbers3/19 Law of sines2/23 Least common multiple16/34 Least squares0/29 Lebesgue integral25/31 Lebesgue measure35/55 Lie algebra50/100 Lie group12/55 Likelihood-ratio test0/11 Limit (mathematics)41/53 Limit inferior and limit superior23/45 Limit of a function36/63 Lindemann–Weierstrass theorem0/17 Linear algebra50/67 Linear equation1/25 Linear map43/72 Linear programming1/49 Linear regression0/47 Linearity4/11 Liouville number13/23 Local ring19/40 Locally convex topological vector space31/82 Logarithm26/53 Logic3/88 Logical conjunction12/21 Logistic function7/59 Löwenheim–Skolem theorem10/17 Lp space32/90 Machine learning1/53 Magic square2/70 Magma (algebra)20/49 Map projection2/48 Margin of error0/24 Markov chain6/75 Martingale (probability theory)12/37 Mathcountsuntagged Mathematical analysis15/39 Mathematical constant13/35 Mathematical induction11/30 Mathematical logic15/83 Mathematical model2/39 Mathematical optimization9/59 Mathematical physics6/22 Mathematical proof6/25 Mathematician0/3 Mathematics6/46 Matrix (mathematics)60/105 Matrix multiplication25/41 Maximal ideal15/31 Maximum and minimum14/23 Maximum likelihood estimation1/67 Maxwell's equations2/65 Mean6/25 Mean value theorem14/23 Measurable function9/19 Median1/71 Metric space64/113 Metric tensor15/56 Minkowski space3/74 Minor (linear algebra)3/22 Möbius function7/26 Möbius strip0/66 Möbius transformation11/98 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/57 Natural logarithm21/37 Natural number40/53 Navier–Stokes equations0/82 Negative number24/33 Newton's method1/54 Nicolas Bourbaki4/7 Nilpotent group12/22 Non-Euclidean geometry4/52 Nondeterministic finite automaton23/38 Norm (mathematics)30/49 Normal distribution17/122 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/37 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 equation3/28 Orientability0/50 Orthogonal group18/101 Orthogonal matrix12/68 Orthogonality4/20 Outer product11/24 P versus NP problem1/56 P-adic number31/86 Parabola1/100 Parallel postulate0/18 Parameter5/37 Pareto distribution2/47 Parity (mathematics)11/33 Partial differential equation2/35 Partial function6/30 Partition of a set11/24 Pauli matrices0/76 Pentagon0/36 Pentagram0/19 Percentage0/24 Perfect graph9/83 Perfect number9/53 Periodic function17/25 Permutation35/90 Perturbation theory (quantum mechanics)9/74 Physics0/57 Pi29/84 Picard–Lindelöf theorem9/18 Pigeonhole principle18/34 Planar graph0/67 Platonic solid0/64 Point (geometry)9/22 Poisson distribution6/84 Poisson manifold0/93 Polygon5/56 Polynomial56/87 Polynomial interpolation12/33 Polytope0/33 Power law1/27 Power series32/52 Presentation of a group5/31 Prime ideal36/75 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 plane7/52 Projective space14/60 Proof that 22/7 exceeds π1/16 Proof theory1/26 Propositional calculus0/73 Propositional logic0/96 Pullback (differential geometry)5/18 Pure mathematics4/19 Putnam Competitionuntagged Pythagorean theorem22/55 Pythagorean triple11/102 Quadratic equation13/62 Quadratic form25/54 Quadratic formula3/17 Quadratic function6/45 Quadratic reciprocity24/58 Quadrilateral2/127 Quantum chromodynamics0/37 Quantum computing0/49 Quantum electrodynamics0/42 Quantum field theory0/60 Quantum mechanics0/63 Quasigroup0/59 Quaternion29/69 Radian3/20 Ramsey's theorem1/94 Random variable24/50 Random walk1/56 Randomness0/21 Rank–nullity theorem8/25 Ratio7/39 Rational function13/28 Real analysis76/98 Real projective line8/23 Real projective space0/29 Rectangle0/39 Recurrence relation9/35 Reflexive space6/66 Register machine0/25 Regression toward the mean0/13 Regular language2/33 Regular polytope0/52 Repeating decimal1/74 Representation theory17/25 Representation theory of finite groups26/113 Ricci calculus11/58 Riemann hypothesis13/110 Riemann integral0/30 Riemann sphere5/35 Riemann surface2/63 Riemann zeta function21/90 Riemannian manifold13/81 Ring (mathematics)97/148 Ring theory22/50 Roman numerals0/55 Root system20/84 Rotation0/20 Sampling (statistics)0/61 Scalar field theory0/50 Schrödinger equation2/59 Schwarzian derivative0/54 Scientific notation0/33 Self-adjoint operator20/75 Separable space16/42 Separation axiom30/59 Sequence58/86 Sequent calculus0/49 Set (mathematics)56/69 Set theory26/44 Seven Bridges of Königsberg5/15 Sheaf (mathematics)26/50 Shor's algorithm3/36 Signal processing1/18 Significant figures0/44 Simple continued fraction15/79 Simplex19/79 Simplex algorithm0/36 Simply typed lambda calculus0/55 Simpson's paradox0/14 Simulated annealing0/53 Singular value decomposition6/74 Slide rule5/33 Sobolev space2/39 Solvable group12/38 Spacetime3/80 Special unitary group4/52 Spectral sequence8/38 Spectral theorem12/35 Spectral theory10/15 Sphere11/62 Sphere packing0/29 Spherical coordinate system1/53 Spherical harmonics2/63 Split-complex number0/47 Square4/74 Square root21/40 Square root of 212/45 Squaring the circle6/43 Standard deviation3/56 Standard Model0/31 Standard probability space4/39 Stationary point6/24 Statistical hypothesis test1/38 Statistical mechanics0/12 Statistical significance0/16 Statistics0/61 Stereographic projection10/50 Stirling number4/28 Stochastic0/5 Stochastic process8/62 Stone–Weierstrass theorem12/24 Straightedge and compass construction0/52 String theory8/93 Structure (mathematical logic)23/49 Student's t-distribution0/43 Student's t-test0/50 Sturm–Liouville theory1/31 Subset21/32 Subtraction7/27 Surface (topology)4/60 Surjective function18/29 Sylow theorems21/33 Symmetric group50/95 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 product30/52 Tessellation1/69 Tesseract0/36 Tetrahedron7/66 Theorem6/33 Theoretical computer science0/31 Theory of relativity0/25 Theta function14/87 Time complexity1/52 Timeline of mathematics45/146 Topological group27/89 Topological space30/42 Topology21/43 Torus4/81 Total order38/50 Transcendental number12/87 Transcendental number theory4/42 Transfinite induction6/7 Trapezoid1/47 Travelling salesman problem0/69 Tree (graph theory)10/43 Triangle33/98 Triangle inequality19/37 Trigonometric functions24/56 Trigonometry12/19 Tuple11/22 Turing machine5/44 Type I and type II errors0/31 Uniform continuity18/33 Uniform convergence25/35 Unitary matrix7/16 Universal enveloping algebra6/33 Variance13/63 Vector bundle19/50 Vector calculus7/26 Vector field7/47 Vector space61/70 Velocity0/42 Von Neumann algebra4/95 Wave1/69 Wave equation0/32 Wavelet1/56 Weil conjectures0/15 Well-order25/47 Winding number1/36 Yang–Mills theory0/31 YBC 72890/7 Yuktibhāṣā7/11 Z-transform0/32 Zermelo–Fraenkel set theory14/34 Zeros and poles7/25 Zorn's lemma28/45