WikiLean

Wikipedia mathematics, mapped to Lean

A mirror of WikiProject Mathematics articles, annotated inline with links into Mathlib4 and color-coded by whether each definition, theorem, and proof has been formalized in Lean. Built by Jack McCarthy.

709 articles 29461 annotated results 28% formalized · 14% partial 50 not yet tagged
formalized partial not formalized
021/35 formalized 110/20 formalized 1002/15 formalized 1729 (number)0/10 formalized 27/14 formalized 33/18 formalized 42/17 formalized 50/30 formalized 61/26 formalized 71/22 formalized 80/19 formalized 92/13 formalized Abacus0/20 formalized Abel Prizenot yet tagged Abelian category21/42 formalized Abelian group38/59 formalized Abelian variety2/43 formalized Absolute value32/52 formalized Abstract algebra19/32 formalized Abstraction0/3 formalized Action (physics)not yet tagged Actuarial science0/5 formalized Addition45/69 formalized Adjoint functors41/61 formalized Adjoint representation6/28 formalized Affine geometry6/25 formalized Affine space40/96 formalized Akaike information criterion0/20 formalized Aleph number17/27 formalized Algebra33/67 formalized Algebra over a field24/40 formalized Algebraic curve4/86 formalized Algebraic geometry16/68 formalized Algebraic K-theory1/102 formalized Algebraic number19/33 formalized Algebraic number field50/77 formalized Algebraic number theory32/56 formalized Algebraic structure31/43 formalized Algebraic topology11/27 formalized Algebraic variety6/54 formalized Algorithm1/50 formalized Altitude (triangle)4/26 formalized American Mathematics Competitions0/7 formalized Analog computer0/18 formalized Analysis of algorithms1/18 formalized Analytic function25/48 formalized Analytic geometry7/38 formalized Analytic number theory15/38 formalized Ancient Greek mathematics9/34 formalized Angle11/55 formalized Arc length8/29 formalized Archimedes Palimpsest0/9 formalized Area11/62 formalized Arithmetic42/92 formalized Arithmetic function36/74 formalized Arithmetic mean7/22 formalized Arithmetical hierarchy1/46 formalized Associative property11/28 formalized Atiyah–Singer index theorem2/38 formalized Average1/20 formalized Axiom4/37 formalized Axiom of choice53/122 formalized Axiom schema of replacement3/20 formalized Banach fixed-point theorem7/16 formalized Banach space61/167 formalized Banach–Tarski paradox3/50 formalized Basis (linear algebra)not yet tagged Bayes' theorem12/29 formalized Bayesian inference7/46 formalized Bayesian probability1/10 formalized Bell's theorem2/23 formalized Big O notation29/56 formalized Bijection20/36 formalized Bijection, injection and surjection22/24 formalized Binary number6/57 formalized Binary search tree0/24 formalized Binary tree9/42 formalized Binomial distribution7/55 formalized Binomial series13/21 formalized Birthday problem0/49 formalized Boolean algebra (structure)25/44 formalized Borel–Kolmogorov paradox0/22 formalized Borel–Weil–Bott theoremnot yet tagged Boundary value problem0/15 formalized Box–Muller transform0/14 formalized Brouwer fixed-point theorem1/31 formalized Butterfly effect0/12 formalized Bézier curve3/48 formalized C*-algebra17/45 formalized Calculus of variations0/47 formalized Cantor's diagonal argument9/22 formalized Cantor's theorem12/16 formalized Cardinal number64/90 formalized Cardinality73/119 formalized Cardinality of the continuum14/25 formalized Cartan connection0/32 formalized Cartesian coordinate system20/52 formalized Category (mathematics)47/57 formalized Category theory10/10 formalized Cauchy sequence14/36 formalized Cauchy's integral formula7/18 formalized Cauchy–Schwarz inequality13/19 formalized Cayley–Hamilton theorem11/42 formalized Cellular automaton0/50 formalized Center squeeze0/21 formalized Central limit theorem7/34 formalized Centroidnot yet tagged Chain rule20/33 formalized Chaos theory1/44 formalized Characteristic class0/13 formalized Characterizations of the exponential functionnot yet tagged Chebyshev polynomials25/70 formalized Chebyshev's inequality7/50 formalized Chern class0/59 formalized Chi-squared distributionnot yet tagged Chinese remainder theorem17/30 formalized Church–Turing thesis2/25 formalized Classical mechanics0/32 formalized Classification of finite simple groups2/36 formalized Clifford algebra37/101 formalized Closed graph theorem (functional analysis)4/26 formalized Cofinality19/37 formalized Coin flipping1/11 formalized Combination18/30 formalized Combinatorial design2/55 formalized Combinatorial game theory0/35 formalized Combinatorics2/34 formalized Combinatory logic0/43 formalized Common logarithmnot yet tagged Commutative algebra10/12 formalized Commutative diagram5/18 formalized Commutative property11/20 formalized Commutative ring82/114 formalized Compact operatornot yet tagged Compact space52/81 formalized Complete metric space41/56 formalized Complex analysis15/22 formalized Complex conjugate14/19 formalized Complex number34/59 formalized Complex plane14/41 formalized Computable function13/34 formalized Computational complexity theory3/45 formalized Computer algebra system4/31 formalized Concrete category9/23 formalized Conditional expectationnot yet tagged Conditional probability8/26 formalized Confidence interval0/9 formalized Conjecture5/33 formalized Conjugacy class18/32 formalized Connected space44/77 formalized Constructible universe0/45 formalized Context-free grammar14/70 formalized Continuous function54/78 formalized Continuum hypothesis6/24 formalized Control theory0/41 formalized Convergence of random variables28/49 formalized Convex set36/67 formalized Convolution26/85 formalized Conway's Game of Life0/52 formalized Cook–Levin theorem0/16 formalized Coordinate system6/42 formalized Coprime integers10/31 formalized Copula (statistics)0/28 formalized Correlation3/40 formalized Cotangent spacenot yet tagged Countable set32/39 formalized Covariance9/30 formalized Covariance and contravariance of vectors23/50 formalized Covariant derivativenot yet tagged Covering space10/77 formalized Coxeter group7/39 formalized Cross product17/50 formalized Cryptography0/52 formalized Cube0/68 formalized Cubic equation7/48 formalized Curl (mathematics)2/35 formalized Curvature0/79 formalized Curvature of Riemannian manifolds0/22 formalized Curve5/49 formalized Cyclic group29/55 formalized Data structure0/13 formalized De Moivre's formula7/21 formalized Decision theory0/14 formalized Derivative34/53 formalized Determinant42/72 formalized Diffeomorphism8/52 formalized Difference engine5/18 formalized Differentiable manifold21/61 formalized Differential calculus16/27 formalized Differential equation1/32 formalized Differential form10/61 formalized Differential geometry3/35 formalized Differential geometry of surfaces6/133 formalized Differential operator6/30 formalized Diophantine approximationnot yet tagged Dirac delta function14/87 formalized Dirac equation1/75 formalized Directed acyclic graph2/52 formalized Discrete calculus18/60 formalized Discrete Fourier transform7/48 formalized Discrete mathematics1/28 formalized Distance12/27 formalized Distribution (mathematical analysis)27/75 formalized Divergence theorem0/16 formalized Division (mathematics)11/30 formalized Division by zero14/40 formalized Divisor16/24 formalized Dot product19/35 formalized Dual space31/66 formalized Duality (mathematics)not yet tagged Dynamic programming0/52 formalized Dynamical system17/86 formalized E (mathematical constant)9/41 formalized Eigenvalues and eigenvectors33/82 formalized Elementary algebra13/55 formalized Ellipse0/92 formalized Elliptic curve23/84 formalized Elliptic function6/14 formalized Elliptic geometry1/45 formalized Elliptic integralnot yet tagged Empty set16/21 formalized Entropy0/53 formalized Equality (mathematics)39/62 formalized Equation solving5/31 formalized Equivalence class20/27 formalized Equivalence relation30/60 formalized Erdős number0/36 formalized Ergodic theory4/27 formalized Erlangen program0/18 formalized Euclid's Elements12/27 formalized Euclidean algorithm43/96 formalized Euclidean distance15/33 formalized Euclidean geometry18/36 formalized Euclidean planes in three-dimensional space1/35 formalized Euclidean space47/72 formalized Euclidean vector23/50 formalized Euler characteristic2/41 formalized Euler's constant3/44 formalized Euler's formula15/23 formalized Euler's identity11/16 formalized Euler's totient function9/43 formalized Expected value29/40 formalized Exponential distribution5/74 formalized Exponential function29/58 formalized Exponential growth2/21 formalized Exponentiation67/104 formalized Exterior algebra21/69 formalized Factorial29/51 formalized Fast Fourier transform1/28 formalized Fermat's Last Theorem13/60 formalized Fermat's little theorem6/17 formalized Fiber bundle10/43 formalized Fibonacci sequence12/63 formalized Fibred category10/44 formalized Field (mathematics)67/86 formalized Field extension36/43 formalized Fields Medal0/1 formalized Finitary relation6/25 formalized Finite difference15/44 formalized Finite field28/54 formalized Finite groupnot yet tagged First-order logic28/95 formalized Five lemma6/8 formalized Flat module24/49 formalized Floor and ceiling functions21/68 formalized Fluid mechanics0/22 formalized Formal language11/27 formalized Formal power seriesnot yet tagged Formula3/10 formalized Four color theorem2/49 formalized Fourier analysis11/28 formalized Fourier series9/32 formalized Fourier transform15/50 formalized Fractal4/32 formalized Fractal dimension1/16 formalized Frame bundle0/34 formalized Fubini's theorem12/28 formalized Function (mathematics)54/82 formalized Functional analysis10/12 formalized Functor24/33 formalized Fundamental group19/76 formalized Fundamental theorem of algebra13/34 formalized Fundamental theorem of arithmetic17/29 formalized Fundamental theorem of calculus7/14 formalized Galois theory5/17 formalized Game theory1/61 formalized Gamma distribution4/90 formalized Gamma function32/89 formalized Gaussian elimination1/28 formalized Gauss–Bonnet theorem0/22 formalized General linear group19/47 formalized General relativity0/62 formalized General topology90/111 formalized Generalized hypergeometric function3/59 formalized Generalized Stokes theorem3/20 formalized Genus (mathematics)0/23 formalized Geodesic2/56 formalized Geometric group theory6/30 formalized Geometric progression4/25 formalized Geometric series11/25 formalized Geometry10/43 formalized Goldbach's conjecture1/34 formalized Golden ratio6/48 formalized Graph (discrete mathematics)28/53 formalized Graph coloring13/157 formalized Graph drawing0/38 formalized Graph minor0/51 formalized Graph of a function5/8 formalized Graph theory12/88 formalized Greatest common divisor33/58 formalized Group (mathematics)42/53 formalized Group action43/78 formalized Group representation15/25 formalized Gödel numbering2/10 formalized Gödel's incompleteness theorems3/66 formalized Haar measure13/43 formalized Ham sandwich theorem0/17 formalized Hamiltonian mechanics0/38 formalized Harmonic analysis1/15 formalized Harmonic function7/30 formalized Hausdorff dimension11/31 formalized Hausdorff space26/39 formalized Hexadecimal1/58 formalized Hexagon0/39 formalized Heyting algebra21/64 formalized Hilbert space83/118 formalized Hilbert's problems2/14 formalized History of algebra15/56 formalized History of geometry1/26 formalized History of mathematical notation6/47 formalized History of mathematics39/111 formalized History of the function concept8/49 formalized Hodge star operatornot yet tagged Holonomy0/37 formalized Hom functor17/20 formalized Homeomorphism4/20 formalized Homological algebra21/26 formalized Homology (mathematics)not yet tagged Homomorphism38/58 formalized Homotopy15/44 formalized Homotopy group4/19 formalized Hopf algebra9/47 formalized Hyperbola0/92 formalized Hyperbolic functionsnot yet tagged Hypercomplex number4/37 formalized Hölder's inequality14/30 formalized Identity function11/15 formalized Imaginary unitnot yet tagged Improper integral7/34 formalized Indian mathematics27/58 formalized Information theory4/33 formalized Inner product space38/50 formalized Integer25/48 formalized Integer factorization3/29 formalized Integral34/70 formalized Interpolation4/35 formalized Interval (mathematics)24/50 formalized Introduction to gauge theory4/30 formalized Introduction to general relativity0/36 formalized Intuitionistic logic5/53 formalized Invariant theory1/19 formalized Inverse trigonometric functions9/35 formalized Invertible matrix12/38 formalized Isomorphism19/37 formalized Isomorphism theorems12/18 formalized Jordan normal form10/60 formalized Kalman filter0/58 formalized Karnaugh map0/24 formalized Kerala school of astronomy and mathematics5/9 formalized Kinematics2/71 formalized Kinetic energy0/33 formalized Klein bottle0/28 formalized Klein four-group5/23 formalized Knot theory0/53 formalized Krull dimension21/43 formalized Kurtosis0/34 formalized L'Hôpital's rule4/26 formalized Lagrange multiplier4/30 formalized Lagrange's theorem (group theory)13/24 formalized Lambert W function0/73 formalized Langlands program0/26 formalized Laplace operatornot yet tagged Laplace transform1/54 formalized Laplace's equation7/56 formalized Lattice (group)not yet tagged Lattice (order)35/61 formalized Law of cosines15/47 formalized Law of large numbers3/19 formalized Law of sines2/23 formalized Least common multiple16/34 formalized Least squares0/29 formalized Lebesgue integral25/31 formalized Lebesgue measure34/54 formalized Lie algebra47/94 formalized Lie group10/46 formalized Likelihood-ratio test0/11 formalized Limit (mathematics)38/50 formalized Limit inferior and limit superior23/45 formalized Limit of a function34/60 formalized Lindemann–Weierstrass theoremnot yet tagged Linear algebra50/67 formalized Linear equation1/25 formalized Linear map40/68 formalized Linear programming1/49 formalized Linear regression0/44 formalized Linearity4/11 formalized Liouville number13/23 formalized Local ringnot yet tagged Locally convex topological vector spacenot yet tagged Logarithm26/53 formalized Logic3/88 formalized Logical conjunction12/21 formalized Logistic function6/56 formalized Lp space29/86 formalized Löwenheim–Skolem theorem10/17 formalized Magic square1/69 formalized Magma (algebra)20/49 formalized Map projection2/48 formalized Margin of error0/23 formalized Markov chain6/75 formalized Martingale (probability theory)12/37 formalized Mathcountsnot yet tagged Mathematical analysis9/33 formalized Mathematical induction10/28 formalized Mathematical logic15/83 formalized Mathematical model1/35 formalized Mathematical optimization9/59 formalized Mathematical physics6/22 formalized Mathematical proof6/25 formalized Mathematician0/3 formalized Mathematics6/46 formalized Matrix (mathematics)52/96 formalized Matrix multiplication25/41 formalized Maximum and minimum14/23 formalized Maximum likelihood estimation1/65 formalized Maxwell's equations2/61 formalized Mean6/25 formalized Mean value theorem14/23 formalized Median1/68 formalized Metric space60/108 formalized Metric tensor15/56 formalized Minkowski space3/74 formalized Minor (linear algebra)3/22 formalized Model theory32/112 formalized Modular arithmetic32/51 formalized Module (mathematics)35/48 formalized Monodromynot yet tagged Monoid42/66 formalized Monte Carlo method1/19 formalized Morphism27/34 formalized Motive (algebraic geometry)0/37 formalized Multiplication41/57 formalized Möbius function7/26 formalized Möbius strip0/66 formalized Möbius transformation11/98 formalized Naive set theorynot yet tagged Nash equilibrium0/56 formalized Natural logarithm21/37 formalized Natural number40/53 formalized Navier–Stokes equations0/73 formalized Negative number24/33 formalized Newton's method1/52 formalized Nicolas Bourbaki4/7 formalized Nilpotent group12/22 formalized Non-Euclidean geometry2/45 formalized Nondeterministic finite automaton23/38 formalized Normal distribution17/113 formalized Normal number0/47 formalized NP-completeness1/27 formalized NP-hardness0/18 formalized Number45/72 formalized Number theory37/64 formalized Numerical analysis2/29 formalized Numerical digit2/19 formalized Numerical integration2/33 formalized Numerical methods for ordinary differential equations1/37 formalized Numerical stability0/13 formalized Nyquist–Shannon sampling theorem0/27 formalized On-Line Encyclopedia of Integer Sequencesnot yet tagged Open set14/39 formalized Operator (mathematics)13/26 formalized Order of magnitude0/25 formalized Ordinal number52/82 formalized Ordinary differential equation3/28 formalized Orthogonal group18/101 formalized Orthogonal matrix12/68 formalized Orthogonality4/20 formalized Outer product11/24 formalized P versus NP problem1/53 formalized P-adic numbernot yet tagged Parabola1/94 formalized Parallel postulate0/18 formalized Parameter5/37 formalized Pareto distributionnot yet tagged Parity (mathematics)11/33 formalized Partial differential equation2/35 formalized Partial function5/28 formalized Partition of a set11/24 formalized Pauli matrices0/76 formalized Pentagon0/36 formalized Pentagram0/16 formalized Percentage0/24 formalized Perfect graph9/83 formalized Perfect number9/52 formalized Periodic function17/25 formalized Permutation35/90 formalized Perturbation theory (quantum mechanics)0/52 formalized Physics0/57 formalized Pi29/83 formalized Picard–Lindelöf theorem9/18 formalized Pigeonhole principle18/34 formalized Planar graph0/67 formalized Platonic solid0/64 formalized Point (geometry)not yet tagged Poisson distribution6/84 formalized Polygon5/56 formalized Polynomial48/79 formalized Polytope0/33 formalized Power law1/24 formalized Power series32/52 formalized Presentation of a group5/31 formalized Prime ideal36/75 formalized Prime number42/85 formalized Primitive recursive function49/95 formalized Principal component analysis1/30 formalized Prisoner's dilemma0/49 formalized Probability16/30 formalized Probability density function14/37 formalized Probability interpretations2/17 formalized Probability space25/37 formalized Probability theory20/36 formalized Product (mathematics)24/29 formalized Product rule11/28 formalized Projective geometry6/28 formalized Projective module21/49 formalized Projective planenot yet tagged Projective space14/60 formalized Proof that 22/7 exceeds π1/16 formalized Proof theory1/26 formalized Propositional logic0/96 formalized Pullback (differential geometry)5/18 formalized Pure mathematics1/10 formalized Putnam Competitionnot yet tagged Pythagorean theorem20/53 formalized Pythagorean triple11/102 formalized Quadratic equation13/58 formalized Quadratic formnot yet tagged Quadratic formula3/17 formalized Quadratic function6/45 formalized Quadratic reciprocity22/55 formalized Quadrilateral2/127 formalized Quantum chromodynamics0/37 formalized Quantum computing0/42 formalized Quantum electrodynamics0/37 formalized Quantum field theory0/51 formalized Quantum mechanics0/59 formalized Quasigroup0/59 formalized Quaternionnot yet tagged Radian3/20 formalized Ramsey's theorem1/90 formalized Random variable17/41 formalized Random walknot yet tagged Randomness0/21 formalized Rank–nullity theorem8/25 formalized Real analysis46/60 formalized Real projective line8/23 formalized Rectangle0/39 formalized Recurrence relation7/33 formalized Reflexive spacenot yet tagged Regression toward the mean0/13 formalized Regular language2/33 formalized Regular polytope0/52 formalized Repeating decimal1/74 formalized Representation theory17/25 formalized Ricci calculus11/58 formalized Riemann hypothesis7/91 formalized Riemann integral0/30 formalized Riemann sphere5/35 formalized Riemann surface2/54 formalized Riemann zeta function21/90 formalized Riemannian manifoldnot yet tagged Ring (mathematics)97/148 formalized Ring theory22/50 formalized Roman numerals0/51 formalized Root system19/81 formalized Rotation0/20 formalized Sampling (statistics)0/49 formalized Scalar field theory0/50 formalized Schrödinger equation2/59 formalized Schwarzian derivative0/54 formalized Scientific notation0/33 formalized Self-adjoint operator20/75 formalized Separable spacenot yet tagged Separation axiom30/59 formalized Sequence58/86 formalized Sequent calculusnot yet tagged Set (mathematics)56/69 formalized Set theory16/34 formalized Seven Bridges of Königsberg5/15 formalized Sheaf (mathematics)23/46 formalized Shor's algorithm3/36 formalized Signal processingnot yet tagged Significant figures0/44 formalized Simple continued fraction15/79 formalized Simplex19/79 formalized Simplex algorithm0/36 formalized Simpson's paradox0/12 formalized Simulated annealing0/51 formalized Singular value decomposition6/68 formalized Slide rule5/33 formalized Solvable group12/38 formalized Spacetime3/72 formalized Special unitary group4/52 formalized Spectral sequence8/38 formalized Spectral theorem11/33 formalized Spectral theory10/15 formalized Sphere11/54 formalized Spherical coordinate system1/53 formalized Spherical harmonics2/63 formalized Split-complex number0/47 formalized Square4/74 formalized Square root21/40 formalized Square root of 212/45 formalized Squaring the circle4/41 formalized Standard deviation2/48 formalized Standard Model0/26 formalized Standard probability space4/39 formalized Stationary point6/24 formalized Statistical hypothesis test0/30 formalized Statistical mechanics0/12 formalized Statistical significancenot yet tagged Statistics0/58 formalized Stereographic projection10/50 formalized Stirling number4/28 formalized Stochastic process8/62 formalized Stone–Weierstrass theorem12/24 formalized Straightedge and compass construction0/52 formalized String theory4/78 formalized Structure (mathematical logic)23/49 formalized Student's t-distribution0/42 formalized Student's t-test0/37 formalized Sturm–Liouville theorynot yet tagged Subset19/30 formalized Subtraction7/27 formalized Surface (topology)4/60 formalized Surjective function18/29 formalized Sylow theorems21/33 formalized Symmetric group50/95 formalized Symmetry4/23 formalized Symmetry (geometry)2/40 formalized Symmetry in mathematics22/46 formalized System of linear equations9/46 formalized Tangent8/36 formalized Tangent bundle12/40 formalized Tangent space12/28 formalized Taylor series20/51 formalized Taylor's theorem25/40 formalized Tensor13/55 formalized Tensor product30/52 formalized Tessellation1/69 formalized Tesseract0/36 formalized Tetrahedron7/66 formalized Theorem6/33 formalized Theoretical computer science0/31 formalized Theory of relativity0/25 formalized Theta function14/87 formalized Time complexity1/48 formalized Timeline of mathematics45/146 formalized Topological group27/89 formalized Topological space30/42 formalized Topology18/39 formalized Total order38/50 formalized Transcendental number9/82 formalized Transfinite induction6/7 formalized Trapezoid1/47 formalized Travelling salesman problem0/69 formalized Tree (graph theory)not yet tagged Trianglenot yet tagged Triangle inequality17/35 formalized Trigonometric functions23/54 formalized Trigonometry12/19 formalized Tuple11/22 formalized Turing machine5/44 formalized Type I and type II errors0/31 formalized Uniform continuity18/33 formalized Uniform convergencenot yet tagged Unitary matrix7/16 formalized Universal enveloping algebranot yet tagged Variance13/63 formalized Vector bundle18/48 formalized Vector calculus7/26 formalized Vector fieldnot yet tagged Vector space61/70 formalized Velocity0/42 formalized Von Neumann algebra4/95 formalized Wave1/68 formalized Wave equation0/32 formalized Wavelet1/54 formalized Weil conjectures0/15 formalized Well-order25/47 formalized Winding number1/36 formalized Yang–Mills theory0/31 formalized YBC 72890/7 formalized Yuktibhāṣā7/11 formalized Z-transform0/32 formalized Zermelo–Fraenkel set theory13/33 formalized Zeros and poles7/25 formalized Zorn's lemma23/38 formalized Étale cohomology3/26 formalized