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
- The Brain — a zoomable map of all of mathematics: every concept joined to its Lean formalization, Wikidata identity, cross-database pages, and literature — with machine-checkable provenance on every edge.
- 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).
- Article graph — articles clustered by shared Mathlib formalizations, colored by their dominant Mathlib area.
- Map — Mathlib's declaration-level dependency edges overlaid on Wikidata's typed statements, on a shared node set.
All articles
formalized
partial
not formalized
0
1
100
1000 (number)
1729 (number)
2
3
4
5
6
7
8
9
Abacus
Abel Prize
Abelian category
Abelian group
Abelian variety
Absolute value
Abstract algebra
Abstraction
Accuracy and precision
Action (physics)
Actuarial science
Addition
Adjoint functors
Adjoint representation
Affine geometry
Affine space
Akaike information criterion
Aleph number
Algebra
Algebra over a field
Algebraic curve
Algebraic geometry
Algebraic K-theory
Algebraic number
Algebraic number field
Algebraic number theory
Algebraic structure
Algebraic topology
Algebraic variety
Algorithm
Altitude (triangle)
American Mathematics Competitions
Analog computer
Analysis of algorithms
Analytic function
Analytic geometry
Analytic number theory
Ancient Greek mathematics
Angle
Applied mathematics
Arc length
Archimedes Palimpsest
Area
Arithmetic
Arithmetic function
Arithmetic mean
Arithmetical hierarchy
Associative property
Asymptotic analysis
Atiyah–Singer index theorem
Automorphic form
Average
Axiom
Axiom of choice
Axiom schema of replacement
Ball (mathematics)
Banach fixed-point theorem
Banach space
Banach–Tarski paradox
Basis (linear algebra)
Bayes' theorem
Bayesian inference
Bayesian probability
Bell's theorem
Bernoulli process
Bézier curve
Big O notation
Bijection
Bijection, injection and surjection
Binary number
Binary search tree
Binary tree
Binomial distribution
Binomial series
Birthday problem
Block design
Boolean algebra (structure)
Borel–Kolmogorov paradox
Borel–Weil–Bott theorem
Boundary value problem
Box–Muller transform
Brouwer fixed-point theorem
Butterfly effect
C*-algebra
Calculus of variations
Cantor's diagonal argument
Cantor's theorem
Cardinal number
Cardinality
Cardinality of the continuum
Cartan connection
Cartesian coordinate system
Category (mathematics)
Category theory
Catenary
Cauchy sequence
Cauchy–Schwarz inequality
Cauchy's integral formula
Cayley–Hamilton theorem
Cellular automaton
Center squeeze
Central limit theorem
Centroid
Chain rule
Chaos theory
Character theory
Characteristic class
Characterizations of the exponential function
Chebyshev polynomials
Chebyshev's inequality
Chern class
Chi-squared distribution
Chinese remainder theorem
Church–Turing thesis
Circle
Circular motion
Classical mechanics
Classical orthogonal polynomials
Classification of finite simple groups
Clifford algebra
Closed graph theorem (functional analysis)
Cofinality
Cohomology
Coin flipping
Combination
Combinatorial design
Combinatorial game theory
Combinatorics
Combinatory logic
Common logarithm
Commutative algebra
Commutative diagram
Commutative property
Commutative ring
Compact group
Compact operator
Compact space
Complete graph
Complete metric space
Complex analysis
Complex conjugate
Complex number
Complex plane
Computable function
Computational complexity theory
Computer algebra system
Concrete category
Conditional expectation
Conditional probability
Confidence interval
Conjecture
Conjugacy class
Connected space
Constructible universe
Context-free grammar
Continuous function
Continuum hypothesis
Control theory
Convergence of random variables
Convex set
Convolution
Conway's Game of Life
Cook–Levin theorem
Coordinate system
Coprime integers
Copula (statistics)
Correlation
Cotangent space
Countable set
Covariance
Covariance and contravariance of vectors
Covariant derivative
Covering space
Coxeter group
Cross product
Cryptography
Cube
Cubic equation
Curl (mathematics)
Curry–Howard correspondence
Curvature
Curvature of Riemannian manifolds
Curve
Cyclic group
Data structure
De Moivre's formula
Decision theory
Derivative
Determinant
Diffeomorphism
Difference engine
Differentiable manifold
Differential calculus
Differential equation
Differential form
Differential geometry
Differential geometry of surfaces
Differential operator
Diophantine approximation
Dirac delta function
Dirac equation
Directed acyclic graph
Discrete calculus
Discrete Fourier transform
Discrete mathematics
Distance
Distribution (mathematical analysis)
Distributive property
Divergence theorem
Divergent series
Division (mathematics)
Division by zero
Divisor
Dot product
Dual space
Duality (mathematics)
Dynamic programming
Dynamical system
E (mathematical constant)
Eigenvalues and eigenvectors
Elementary algebra
Ellipse
Elliptic curve
Elliptic function
Elliptic geometry
Elliptic integral
Empty set
Entropy
Entropy (information theory)
Equality (mathematics)
Equation solving
Equivalence class
Equivalence relation
Erdős number
Ergodic theory
Erlangen program
Étale cohomology
Euclid's Elements
Euclidean algorithm
Euclidean distance
Euclidean geometry
Euclidean group
Euclidean planes in three-dimensional space
Euclidean space
Euclidean vector
Euler characteristic
Euler's constant
Euler's formula
Euler's identity
Euler's theorem
Euler's totient function
Expected value
Experimental mathematics
Exponential distribution
Exponential function
Exponential growth
Exponentiation
Exterior algebra
Factorial
Fast Fourier transform
Fermat's Last Theorem
Fermat's little theorem
Fiber bundle
Fibonacci sequence
Fibred category
Field (mathematics)
Field extension
Fields Medal
Finitary relation
Finite difference
Finite field
Finite group
First-order logic
Five lemma
Flat module
Floor and ceiling functions
Fluid mechanics
Formal language
Formal power series
Formula
Four color theorem
Fourier analysis
Fourier series
Fourier transform
Fractal
Fractal dimension
Frame bundle
Fubini's theorem
Function (mathematics)
Functional analysis
Functor
Fundamental group
Fundamental theorem of algebra
Fundamental theorem of arithmetic
Fundamental theorem of calculus
Galois theory
Game theory
Gamma distribution
Gamma function
Gauss–Bonnet theorem
Gaussian elimination
General linear group
General relativity
General topology
Generalized hypergeometric function
Generalized Riemann hypothesis
Generalized Stokes theorem
Genus (mathematics)
Geodesic
Geometric group theory
Geometric progression
Geometric series
Geometry
Gibbs phenomenon
Gödel numbering
Gödel's incompleteness theorems
Goldbach's conjecture
Golden ratio
Gradient
Graph (discrete mathematics)
Graph coloring
Graph drawing
Graph minor
Graph of a function
Graph theory
Greatest common divisor
Group (mathematics)
Group action
Group representation
Haar measure
Hahn–Banach theorem
Hairy ball theorem
Ham sandwich theorem
Hamiltonian mechanics
Harmonic analysis
Harmonic function
Hausdorff dimension
Hausdorff space
Hexadecimal
Hexagon
Heyting algebra
Hilbert space
Hilbert's problems
History of algebra
History of geometry
History of mathematical notation
History of mathematics
History of the function concept
Hodge star operator
Hölder's inequality
Holonomy
Hom functor
Homeomorphism
Homogeneous space
Homological algebra
Homology (mathematics)
Homomorphism
Homotopy
Homotopy group
Hopf algebra
Hyperbola
Hyperbolic functions
Hypercomplex number
Identity function
Imaginary unit
Improper integral
Indian mathematics
Information theory
Inner product space
Integer
Integer factorization
Integral
Interpolation
Interval (mathematics)
Introduction to gauge theory
Introduction to general relativity
Intuitionistic logic
Invariant theory
Inverse trigonometric functions
Invertible matrix
Isomorphism
Isomorphism theorems
Jordan normal form
Kalman filter
Karnaugh map
Kepler's laws of planetary motion
Kerala school of astronomy and mathematics
Kinematics
Kinetic energy
Klein bottle
Klein four-group
Knot theory
Kronecker delta
Krull dimension
Kullback–Leibler divergence
Kurtosis
L'Hôpital's rule
Lagrange multiplier
Lagrange's theorem (group theory)
Lambert W function
Langlands program
Laplace operator
Laplace transform
Laplace's equation
Latitude
Lattice (group)
Lattice (order)
Law of cosines
Law of large numbers
Law of sines
Least common multiple
Least squares
Lebesgue integral
Lebesgue measure
Lie algebra
Lie group
Likelihood-ratio test
Limit (mathematics)
Limit inferior and limit superior
Limit of a function
Lindemann–Weierstrass theorem
Linear algebra
Linear equation
Linear map
Linear programming
Linear regression
Linearity
Liouville number
Local ring
Locally convex topological vector space
Logarithm
Logic
Logical conjunction
Logistic function
Löwenheim–Skolem theorem
Lp space
Machine learning
Magic square
Magma (algebra)
Map projection
Margin of error
Markov chain
Martingale (probability theory)
Mathcounts
Mathematical analysis
Mathematical constant
Mathematical induction
Mathematical logic
Mathematical model
Mathematical optimization
Mathematical physics
Mathematical proof
Mathematician
Mathematics
Matrix (mathematics)
Matrix multiplication
Maximal ideal
Maximum and minimum
Maximum likelihood estimation
Maxwell's equations
Mean
Mean value theorem
Measurable function
Median
Metric space
Metric tensor
Minkowski space
Minor (linear algebra)
Möbius function
Möbius strip
Möbius transformation
Model theory
Modular arithmetic
Module (mathematics)
Monodromy
Monoid
Monte Carlo method
Morphism
Motive (algebraic geometry)
Multiplication
Naive set theory
Nash equilibrium
Natural logarithm
Natural number
Navier–Stokes equations
Negative number
Newton's method
Nicolas Bourbaki
Nilpotent group
Non-Euclidean geometry
Nondeterministic finite automaton
Norm (mathematics)
Normal distribution
Normal number
NP-completeness
NP-hardness
Number
Number theory
Numerical analysis
Numerical digit
Numerical integration
Numerical methods for ordinary differential equations
Numerical stability
Nyquist–Shannon sampling theorem
On-Line Encyclopedia of Integer Sequences
Open set
Operator (mathematics)
Order of magnitude
Ordinal number
Ordinary differential equation
Orientability
Orthogonal group
Orthogonal matrix
Orthogonality
Outer product
P versus NP problem
P-adic number
Parabola
Parallel postulate
Parameter
Pareto distribution
Parity (mathematics)
Partial differential equation
Partial function
Partition of a set
Pauli matrices
Pentagon
Pentagram
Percentage
Perfect graph
Perfect number
Periodic function
Permutation
Perturbation theory (quantum mechanics)
Physics
Pi
Picard–Lindelöf theorem
Pigeonhole principle
Planar graph
Platonic solid
Point (geometry)
Poisson distribution
Poisson manifold
Polygon
Polynomial
Polynomial interpolation
Polytope
Power law
Power series
Presentation of a group
Prime ideal
Prime number
Primitive recursive function
Principal component analysis
Prisoner's dilemma
Probability
Probability density function
Probability interpretations
Probability space
Probability theory
Product (mathematics)
Product rule
Projective geometry
Projective module
Projective plane
Projective space
Proof that 22/7 exceeds π
Proof theory
Propositional calculus
Propositional logic
Pullback (differential geometry)
Pure mathematics
Putnam Competition
Pythagorean theorem
Pythagorean triple
Quadratic equation
Quadratic form
Quadratic formula
Quadratic function
Quadratic reciprocity
Quadrilateral
Quantum chromodynamics
Quantum computing
Quantum electrodynamics
Quantum field theory
Quantum mechanics
Quasigroup
Quaternion
Radian
Ramsey's theorem
Random variable
Random walk
Randomness
Rank–nullity theorem
Ratio
Rational function
Real analysis
Real projective line
Real projective space
Rectangle
Recurrence relation
Reflexive space
Register machine
Regression toward the mean
Regular language
Regular polytope
Repeating decimal
Representation theory
Representation theory of finite groups
Ricci calculus
Riemann hypothesis
Riemann integral
Riemann sphere
Riemann surface
Riemann zeta function
Riemannian manifold
Ring (mathematics)
Ring theory
Roman numerals
Root system
Rotation
Sampling (statistics)
Scalar field theory
Schrödinger equation
Schwarzian derivative
Scientific notation
Self-adjoint operator
Separable space
Separation axiom
Sequence
Sequent calculus
Set (mathematics)
Set theory
Seven Bridges of Königsberg
Sheaf (mathematics)
Shor's algorithm
Signal processing
Significant figures
Simple continued fraction
Simplex
Simplex algorithm
Simply typed lambda calculus
Simpson's paradox
Simulated annealing
Singular value decomposition
Slide rule
Sobolev space
Solvable group
Spacetime
Special unitary group
Spectral sequence
Spectral theorem
Spectral theory
Sphere
Sphere packing
Spherical coordinate system
Spherical harmonics
Split-complex number
Square
Square root
Square root of 2
Squaring the circle
Standard deviation
Standard Model
Standard probability space
Stationary point
Statistical hypothesis test
Statistical mechanics
Statistical significance
Statistics
Stereographic projection
Stirling number
Stochastic
Stochastic process
Stone–Weierstrass theorem
Straightedge and compass construction
String theory
Structure (mathematical logic)
Student's t-distribution
Student's t-test
Sturm–Liouville theory
Subset
Subtraction
Surface (topology)
Surjective function
Sylow theorems
Symmetric group
Symmetry
Symmetry (geometry)
Symmetry in mathematics
Synthetic geometry
System F
System of linear equations
Tangent
Tangent bundle
Tangent space
Taylor series
Taylor's theorem
Tensor
Tensor product
Tessellation
Tesseract
Tetrahedron
Theorem
Theoretical computer science
Theory of relativity
Theta function
Time complexity
Timeline of mathematics
Topological group
Topological space
Topology
Torus
Total order
Transcendental number
Transcendental number theory
Transfinite induction
Trapezoid
Travelling salesman problem
Tree (graph theory)
Triangle
Triangle inequality
Trigonometric functions
Trigonometry
Tuple
Turing machine
Type I and type II errors
Uniform continuity
Uniform convergence
Unitary matrix
Universal enveloping algebra
Variance
Vector bundle
Vector calculus
Vector field
Vector space
Velocity
Von Neumann algebra
Wave
Wave equation
Wavelet
Weil conjectures
Well-order
Winding number
Yang–Mills theory
YBC 7289
Yuktibhāṣā
Z-transform
Zermelo–Fraenkel set theory
Zeros and poles
Zorn's lemma