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.

254 articles 12093 annotated results 22% formalized · 16% partial 1 not yet tagged

formalized partial not formalized

→ Wikidata concept links — every formalized concept keyed to its Wikidata item, as an open RDF dataset (the basis for a proposed “formalized as (Lean/Mathlib)” Wikidata property).

Hide untagged

021/35 formalized 110/20 formalized 27/14 formalized 42/17 formalized 50/30 formalized Abacus0/20 formalized Abel Prizenot yet tagged Abelian group38/59 formalized Algebraic geometry16/68 formalized Algebraic K-theory1/102 formalized Algebraic number19/33 formalized Algebraic number theory32/56 formalized Algebraic topology11/27 formalized Algebraic variety6/54 formalized Algorithm1/50 formalized American Mathematics Competitions0/7 formalized Analysis of algorithms1/18 formalized Ancient Greek mathematics9/34 formalized Angle11/55 formalized Arithmetic42/92 formalized Atiyah–Singer index theorem2/38 formalized Axiom4/37 formalized Banach fixed-point theorem7/16 formalized Bayes' theorem12/29 formalized Bijection, injection and surjection22/24 formalized Binary search tree0/24 formalized Binomial distribution7/55 formalized Boolean algebra (structure)25/44 formalized Brouwer fixed-point theorem1/31 formalized Bézier curve3/48 formalized C*-algebra17/45 formalized Calculus of variations0/47 formalized Cantor's diagonal argument9/22 formalized Cardinality73/119 formalized Cardinality of the continuum14/25 formalized Category (mathematics)47/57 formalized Cayley–Hamilton theorem11/42 formalized Center squeeze0/21 formalized Chaos theory1/44 formalized Chern class0/59 formalized Chinese remainder theorem17/30 formalized Classical mechanics0/32 formalized Combinatorial design2/55 formalized Complete metric space41/56 formalized Computable function13/34 formalized Computational complexity theory3/45 formalized Conjecture5/33 formalized Continuum hypothesis6/24 formalized Control theory0/41 formalized Convex set36/67 formalized Conway's Game of Life0/52 formalized Cook–Levin theorem0/16 formalized Countable set32/39 formalized Coxeter group7/39 formalized Cryptography0/52 formalized Data structure0/13 formalized De Moivre's formula7/21 formalized Diffeomorphism8/52 formalized Difference engine5/18 formalized Differential calculus16/27 formalized Differential equation1/32 formalized Differential geometry3/35 formalized Differential geometry of surfaces6/133 formalized Dirac equation1/75 formalized Directed acyclic graph2/52 formalized Discrete calculus18/60 formalized Discrete mathematics1/28 formalized Distribution (mathematical analysis)27/75 formalized Dual space31/66 formalized Elementary algebra13/55 formalized Elliptic curve23/84 formalized Elliptic geometry1/45 formalized Equality (mathematics)39/62 formalized Erdős number0/36 formalized Euclidean algorithm43/96 formalized Euclidean geometry18/36 formalized Exponential function29/58 formalized Fibred category10/44 formalized Fields Medal0/1 formalized First-order logic28/95 formalized Fluid mechanics0/22 formalized Formula3/10 formalized Four color theorem2/49 formalized Fourier analysis11/28 formalized Fractal4/32 formalized Functor24/33 formalized Game theory1/61 formalized General relativity0/62 formalized General topology90/111 formalized Geodesic2/56 formalized Geometric group theory6/30 formalized Geometry10/43 formalized Graph coloring13/157 formalized Graph drawing0/38 formalized Graph minor0/51 formalized Graph theory12/88 formalized Greatest common divisor33/58 formalized Group action43/78 formalized Group representation15/25 formalized Gödel's incompleteness theorems3/66 formalized Hausdorff space26/39 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 Holonomy0/37 formalized Hom functor17/20 formalized Homological algebra21/26 formalized Homomorphism38/58 formalized Hyperbola0/92 formalized Indian mathematics27/58 formalized Information theory4/33 formalized Integer25/48 formalized Interpolation4/35 formalized Introduction to gauge theory4/30 formalized Introduction to general relativity0/36 formalized Jordan normal form10/60 formalized Kerala school of astronomy and mathematics5/9 formalized Kinematics2/71 formalized Kinetic energy0/33 formalized Knot theory0/53 formalized Krull dimension21/43 formalized Lambert W function0/73 formalized Laplace transform1/54 formalized Least squares0/29 formalized Linear equation1/25 formalized Linear programming1/49 formalized Linear regression0/44 formalized Logic3/88 formalized Margin of error0/23 formalized Mathematical logic15/83 formalized Mathematical optimization9/59 formalized Mathematical physics6/22 formalized Mathematician0/3 formalized Mathematics6/46 formalized Maximum likelihood estimation1/65 formalized Maxwell's equations2/61 formalized Mean6/25 formalized Median1/68 formalized Minkowski space3/74 formalized Model theory32/112 formalized Module (mathematics)35/48 formalized Monte Carlo method1/19 formalized Möbius strip0/66 formalized Nash equilibrium0/56 formalized Navier–Stokes equations0/73 formalized Nicolas Bourbaki4/7 formalized Non-Euclidean geometry2/45 formalized Nondeterministic finite automaton23/38 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 Operator (mathematics)13/26 formalized Order of magnitude0/25 formalized Ordinal number52/82 formalized Orthogonal group18/101 formalized Orthogonal matrix12/68 formalized P versus NP problem1/53 formalized Parabola1/94 formalized Parameter5/37 formalized Perfect graph9/83 formalized Permutation35/90 formalized Perturbation theory (quantum mechanics)0/52 formalized Physics0/57 formalized Picard–Lindelöf theorem9/18 formalized Pigeonhole principle18/34 formalized Poisson distribution6/84 formalized Power series32/52 formalized Presentation of a group5/31 formalized Prime ideal36/75 formalized Probability density function14/37 formalized Probability interpretations2/17 formalized Probability space25/37 formalized Probability theory20/36 formalized Projective module21/49 formalized Projective space14/60 formalized Propositional logic0/96 formalized Pure mathematics1/10 formalized Quadratic formula3/17 formalized Quadratic reciprocity22/55 formalized Quantum electrodynamics0/37 formalized Quantum field theory0/51 formalized Quantum mechanics0/59 formalized Ramsey's theorem1/90 formalized Randomness0/21 formalized Real projective line8/23 formalized Ricci calculus11/58 formalized Riemann sphere5/35 formalized Riemann surface2/54 formalized Riemann zeta function21/90 formalized Ring theory22/50 formalized Root system19/81 formalized Sampling (statistics)0/49 formalized Scalar field theory0/50 formalized Scientific notation0/33 formalized Self-adjoint operator20/75 formalized Set theory16/34 formalized Simplex19/79 formalized Simulated annealing0/51 formalized Singular value decomposition6/68 formalized Slide rule5/33 formalized Spacetime3/72 formalized Spectral sequence8/38 formalized Spectral theorem11/33 formalized Spectral theory10/15 formalized Spherical coordinate system1/53 formalized Split-complex number0/47 formalized Square4/74 formalized Square root of 212/45 formalized Squaring the circle4/41 formalized Standard probability space4/39 formalized Stationary point6/24 formalized Statistical hypothesis test0/30 formalized Statistics0/58 formalized Stirling number4/28 formalized Student's t-distribution0/42 formalized Student's t-test0/37 formalized Surface (topology)4/60 formalized Surjective function18/29 formalized Symmetric group50/95 formalized Symmetry (geometry)2/40 formalized Symmetry in mathematics22/46 formalized System of linear equations9/46 formalized Tangent bundle8/35 formalized Tangent space12/28 formalized Taylor's theorem25/40 formalized Tessellation1/69 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 Topology18/39 formalized Transcendental number9/82 formalized Triangle inequality17/35 formalized Trigonometry12/19 formalized Turing machine5/44 formalized Type I and type II errors0/31 formalized Vector bundle18/48 formalized Vector calculus7/26 formalized Von Neumann algebra4/95 formalized Wave1/68 formalized Wavelet1/54 formalized Well-order25/47 formalized Winding number1/36 formalized Yang–Mills theory0/31 formalized YBC 72890/7 formalized Yuktibhāṣā7/11 formalized Zorn's lemma23/38 formalized