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
36,861annotated results
27%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/20 1000 (number)0/89 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/35 Action (physics)0/27 Actuarial science0/5 Addition49/77 Adjoint functors44/64 Adjoint representation7/32 Affine geometry6/25 Affine space43/100 Akaike information criterion0/20 Aleph number17/27 Algebra33/67 Algebra over a field28/44 Algebraic curve4/86 Algebraic geometry16/68 Algebraic K-theory1/102 Algebraic number19/33 Algebraic number field61/88 Algebraic number theory32/56 Algebraic structure31/43 Algebraic topology11/27 Algebraic variety6/54 Algebraically closed field31/63 Algorithm1/50 Almagest0/120 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 length10/33 Archimedes Palimpsest0/9 Area11/62 Arithmetic42/92 Arithmetic function36/74 Arithmetic mean7/22 Arithmetical hierarchy1/48 Associative property11/28 Asymptotic analysis9/25 Atiyah–Singer index theorem2/38 Automorphic form1/9 Average1/24 Axiom4/37 Axiom of choice53/125 Axiom schema of replacement3/20 Ball (mathematics)17/31 Banach fixed-point theorem9/19 Banach space61/168 Banach–Tarski paradox3/50 Basis (linear algebra)32/47 Bayes' theorem12/29 Bayesian inference7/46 Bayesian probability1/10 Bell's theorem4/41 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/51 Borel–Kolmogorov paradox0/22 Borel–Weil–Bott theorem0/18 Boundary value problem0/15 Box–Muller transform0/17 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 continuum18/29 Cartan connection0/32 Cartesian coordinate system23/61 Category (mathematics)56/66 Category theory10/10 Catenary0/35 Cauchy sequence14/36 Cauchy–Schwarz inequality27/33 Cauchy's integral formula9/20 Cayley–Hamilton theorem11/42 Cellular automaton1/73 Center squeeze0/21 Central limit theorem19/49 Centroid5/45 Chain rule20/33 Chaos theory2/46 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/38 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 Combinatorics12/51 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 number46/71 Complex plane14/41 Computable function13/34 Computational complexity theory5/66 Computer algebra system7/35 Concrete category9/23 Conditional expectation26/40 Conditional probability8/26 Confidence interval0/9 Conjecture2/33 Conjugacy class18/32 Connected space44/77 Constructible universe0/46 Context-free grammar15/72 Continuous function82/106 Continuum hypothesis9/29 Control theory0/41 Convergence of random variables28/49 Convex set36/69 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 set44/54 Covariance9/30 Covariance and contravariance of vectors23/50 Covariant derivative8/48 Covering space12/83 Coxeter group7/39 Cross product17/50 Cryptography0/52 Cube3/80 Cubic equation7/48 Curl (mathematics)2/53 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 theory0/14 Derivative34/53 Determinant56/93 Diffeomorphism9/53 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)19/41 Division by zero14/40 Divisor30/41 Dot product21/40 Dual space34/69 Duality (mathematics)49/106 Dynamic programming0/52 Dynamical system30/106 E (mathematical constant)21/60 Eigenvalues and eigenvectors42/92 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 Elements17/46 Euclidean algorithm43/96 Euclidean distance15/33 Euclidean geometry23/47 Euclidean group0/26 Euclidean planes in three-dimensional space1/35 Euclidean space51/79 Euclidean vector23/50 Euler angles0/100 Euler characteristic2/41 Euler's constant3/49 Euler's formula27/36 Euler's identity11/16 Euler's theorem3/6 Euler's totient function13/48 Expected value29/40 Experimental mathematics0/24 Exponential distribution5/80 Exponential function29/58 Exponential growth1/24 Exponentiation71/111 Exterior algebra21/75 Factorial36/61 Fast Fourier transform1/28 Fermat's Last Theorem17/71 Fermat's little theorem6/17 Fiber bundle11/46 Fibonacci sequence17/74 Fibred category10/44 Field (mathematics)80/107 Field extension45/55 Fields Medal0/1 Finitary relation8/28 Finite difference22/53 Finite field31/57 Finite group14/24 First-order logic28/95 Five lemma6/8 Flat module24/49 Floor and ceiling functions22/70 Fluid mechanics0/31 Formal language11/27 Formal power series42/82 Formula3/10 Four color theorem2/49 Fourier analysis11/28 Fourier series11/36 Fourier transform29/76 Fractal5/40 Fractal dimension1/16 Frame bundle0/34 Fubini's theorem12/28 Function (mathematics)64/92 Functional analysis10/12 Functor33/42 Fundamental group19/76 Fundamental theorem of algebra13/34 Fundamental theorem of arithmetic17/29 Fundamental theorem of calculus7/14 Galois theory20/34 Game theory1/61 Gamma distribution4/92 Gamma function33/95 Gauss–Bonnet theorem0/22 Gaussian elimination1/31 General linear group19/47 General relativity0/62 General topology90/111 Generalized hypergeometric function11/76 Generalized Riemann hypothesis5/37 Generalized Stokes theorem3/20 Genus (mathematics)0/29 Geodesic2/56 Geometric group theory7/47 Geometric progression7/31 Geometric series11/25 Geometry10/43 Gibbs phenomenon0/20 Gödel numbering2/10 Gödel's incompleteness theorems5/75 Goldbach's conjecture2/44 Golden ratio7/52 Gradient8/43 Graph (discrete mathematics)28/53 Graph coloring13/157 Graph drawing0/38 Graph minor0/55 Graph of a function5/8 Graph theory28/131 Greatest common divisor33/58 Group (mathematics)54/66 Group action44/81 Group representation18/28 Haar measure13/43 Hahn–Banach theorem9/54 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 space93/129 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/57 Hodge star operator1/53 Hölder's inequality16/32 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 functions31/62 Hyperbolic geometry4/231 Hypercomplex number4/37 Identity function11/15 Imaginary unit16/43 Improper integral7/34 Indian mathematics27/58 Information theory4/33 Inner product space41/52 Integer25/48 Integer factorization3/29 Integral32/75 Interpolation4/35 Interval (mathematics)29/58 Introduction to gauge theory4/30 Introduction to general relativity0/36 Intuitionistic logic12/63 Invariant theory1/19 Inverse trigonometric functions12/40 Inversive geometry20/131 Invertible matrix20/48 Isomorphism30/49 Isomorphism theorems13/23 Jordan normal form11/61 Kalman filter0/73 Karnaugh map0/29 Kepler's laws of planetary motion0/47 Kerala school of astronomy and mathematics5/9 Kinematics2/71 Kinetic energy0/33 Klein bottle0/28 Klein four-group11/33 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)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 measure36/58 Lie algebra55/105 Lie group12/58 Likelihood-ratio test0/11 Limit (mathematics)44/59 Limit inferior and limit superior26/48 Limit of a function39/66 Lindemann–Weierstrass theorem0/17 Linear algebra50/67 Linear equation1/25 Linear map48/79 Linear programming2/54 Linear regression3/55 Linearity4/11 Liouville number13/23 Local ring19/40 Locally convex topological vector space37/89 Logarithm38/75 Logic3/88 Logical conjunction12/21 Logistic function7/59 Löwenheim–Skolem theorem10/17 Lp space38/97 Machine learning3/58 Magic square2/70 Magma (algebra)20/49 Map projection2/48 Margin of error0/28 Markov chain6/75 Martingale (probability theory)16/42 Mathcountsuntagged Mathematical analysis30/62 Mathematical constant17/41 Mathematical induction11/30 Mathematical logic15/83 Mathematical model6/56 Mathematical optimization9/59 Mathematical physics6/22 Mathematical proof6/25 Mathematician0/3 Mathematics15/67 Matrix (mathematics)60/105 Matrix multiplication25/41 Maximal ideal18/34 Maximum and minimum14/23 Maximum likelihood estimation1/67 Maxwell's equations2/65 Mean6/25 Mean value theorem16/25 Measurable function9/19 Median1/71 Metric space72/126 Metric tensor15/56 Minkowski space3/74 Minor (linear algebra)3/22 Möbius function10/31 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/63 Natural logarithm21/37 Natural number48/61 Navier–Stokes equations0/82 Negative number24/33 Newton's method2/70 Nicolas Bourbaki4/7 Nilpotent group12/22 Non-Euclidean geometry5/56 Nondeterministic finite automaton23/38 Nonlinear programmingpending Norm (mathematics)30/49 Normal distribution18/125 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/43 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/105 Orthogonal matrix12/68 Orthogonality4/20 Outer product11/24 P versus NP problem1/57 P-adic number34/89 Parabola1/100 Parallel postulate0/18 Parameter5/37 Pareto distribution2/47 Parity (mathematics)11/33 Partial differential equation2/35 Partial function6/32 Partition of a set11/24 Pauli matrices0/79 Pell number0/6 Pentagon0/36 Pentagram2/24 Percentage0/24 Perfect graph9/83 Perfect number9/53 Periodic function20/29 Permutation35/90 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 Polynomial58/91 Polynomial interpolation12/33 Polytope0/33 Power law1/38 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/55 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 mathematics11/28 Putnam Competitionuntagged Pythagorean theorem22/55 Pythagorean triple13/106 Quadratic equation13/71 Quadratic form32/62 Quadratic formula3/17 Quadratic function6/45 Quadratic reciprocity28/64 Quadratic sievepending Quadrilateral2/127 Quantum chromodynamics0/37 Quantum computing1/60 Quantum electrodynamics0/42 Quantum field theory0/60 Quantum mechanics0/63 Quasigroup0/59 Quaternion29/73 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 function14/31 Real analysis83/106 Real projective line8/23 Real projective space0/29 Rectangle0/39 Recurrence relation9/42 Reflexive space6/66 Register machine2/31 Regression toward the mean1/15 Regular language2/33 Regular polytope0/52 Repeating decimal4/79 Representation theory17/25 Representation theory of finite groups32/121 Ricci calculus11/58 Riemann hypothesis14/111 Riemann integral0/30 Riemann sphere5/35 Riemann surface2/63 Riemann zeta function21/90 Riemannian manifold13/86 Riesz representation theorempending Ring (mathematics)97/148 Ring theory22/50 Roman numerals0/55 Root system22/95 Rotation0/20 Sampling (statistics)0/69 Scalar field theory0/50 Scalar multiplication27/41 Schrödinger equation2/59 Schwarzian derivative0/54 Scientific notation0/33 Second-order logic2/62 Self-adjoint operator20/75 Separable space16/42 Separation axiom30/59 Sequence58/86 Sequent calculus0/61 Set (mathematics)54/69 Set theory26/44 Seven Bridges of Königsberg9/19 Sheaf (mathematics)26/50 Shor's algorithm3/36 Signal processing1/18 Significant figures1/47 Simple continued fraction15/79 Simplex19/79 Simplex algorithm0/36 Simply typed lambda calculus0/55 Simpson's paradox0/15 Simulated annealing0/53 Singular value decomposition16/99 Slide rule5/33 Sobolev space2/39 Solvable group12/38 Spacetime3/80 Special unitary group4/55 Spectral sequence8/38 Spectral theorem12/35 Spectral theory10/15 Sphere10/64 Sphere packing0/29 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 deviation4/59 Standard Model0/31 Standard probability space4/39 Stationary point6/24 Statistical hypothesis test0/46 Statistical mechanics0/12 Statistical significance0/16 Statistics0/64 Stereographic projection10/50 Stirling number4/28 Stochastic0/5 Stochastic process8/62 Stone–Weierstrass theorem13/25 Straightedge and compass construction0/52 String theory8/93 Structure (mathematical logic)23/49 Student's t-distribution0/49 Student's t-test0/68 Sturm–Liouville theory1/31 Subset21/32 Subtraction7/27 Surface (topology)4/60 Surjective function18/29 Sylow theorems25/37 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 product31/56 Tessellation1/69 Tesseract0/36 Tetrahedron7/66 Theorem6/33 Theoretical computer science0/31 Theory of relativity0/25 Theta function14/87 Time complexity5/58 Timeline of mathematics45/146 Topological group27/89 Topological space30/42 Topology21/43 Torus4/81 Total order38/50 Transcendental number15/90 Transcendental number theory4/42 Transfinite induction6/7 Trapezoid1/47 Travelling salesman problem0/69 Tree (graph theory)10/43 Triangle39/105 Triangle inequality23/41 Trigonometric functions24/58 Trigonometry12/19 Tuple11/22 Turing machine5/44 Type I and type II errors0/31 Type theory2/87 Uniform continuity18/33 Uniform convergence33/43 Unitary matrix7/16 Universal enveloping algebra8/36 Variance13/63 Vector bundle19/50 Vector calculus7/26 Vector field12/56 Vector space61/70 Velocity0/42 Von Neumann algebra4/95 Wave1/70 Wave equation0/32 Wavelet1/56 Weil conjectures0/15 Well-order26/48 Winding number1/36 Yang–Mills theory0/31 YBC 72890/7 Yuktibhāṣā7/11 Z-transform0/32 Zermelo–Fraenkel set theory14/38 Zeros and poles7/25 Zorn's lemma47/69