Formalized theorems

MSC	Name	Isabelle	HOL Light	Coq	Lean	Metamath	Mizar
05	Hales–Jewett theorem				L
03	Cantor–Bernstein–Schroeder theorem	S	S	X	L	L	L
30	Identity theorem				L
05	Turán's theorem				L
26	Cantor's intersection theorem				L
30	Hartogs's theorem				X
54	Baire category theorem				L
20	Sylow theorems				L
26	Squeeze theorem				L
16	Isomorphism theorem				L
28	Dominated convergence theorem				L
28	Bounded convergence theorem				L
46	Closed graph theorem				L
03	Löwenheim–Skolem theorem				L
14	Hilbert's Nullstellensatz (theorem of zeroes)				L
11	Euler's partition theorem				L
11	Apéry's theorem				X
11	Minkowski's theorem				L
28	Vitali convergence theorem				L
54	Tychonoff's theorem				L
26	Taylor's theorem				L
20	Cauchy's theorem				L
54	Brouwer fixed-point theorem				X
28	Fubini's theorem				L
03	Compactness theorem				L
51	Pythagorean theorem				L
26	Monotone convergence theorem				L
11	Lucas's theorem				L
16	Fundamental theorem on homomorphisms				L
11	Zeckendorf's theorem				L
28	Radon–Nikodym theorem				L
28	Egorov's theorem				L
54	Metrization theorems				L
26	Fundamental theorem of calculus				L
15	Birkhoff–Von Neumann theorem				L
20	Nielsen–Schreier theorem				L
57	Whitney embedding theorem				L
11	Fermat's Last Theorem				L
54	Tietze extension theorem				L
26	Besicovitch covering theorem				L
46	Banach–Steinhaus theorem				L
03	Well-ordering theorem				L
46	Arzelà–Ascoli theorem				L
11	Euclid's theorem				L
05	Hindman's theorem				L
28	Hahn decomposition theorem				L
03	Matiyasevich's theorem				L
52	Helly's theorem				L
05	Sprague–Grundy theorem				L
06	Birkhoff's representation theorem				L
13	Lasker–Noether theorem				L
11	Sylvester's law of inertia				L
68	Smn theorem				L
20	Cayley's theorem				L
12	Rational root theorem				L
12	Integral root theorem				L
20	Schur's lemma				L
11	Euclid–Euler theorem				L
60	Bayes' theorem				L
11	Fermat's little theorem				L
26	Mean value theorem				L
68	Rice's theorem				L
30	De Moivre's theorem				L
54	Lebesgue's decomposition theorem				L
30	Fundamental theorem of algebra				L
26	Rolle's theorem				L
03	Kleene's recursion theorem				L
11	Chinese remainder theorem				L
03	Gödel's incompleteness theorem				X
60	Optional stopping theorem				L
12	Solutions of a general cubic equation				L
03	Independence of the continuum hypothesis				X
12	Primitive element theorem				L
54	Banach fixed-point theorem				L
05	Sperner's theorem				L
20	Schur–Zassenhaus theorem				L
60	Bertrand's ballot theorem				L
26	Lebesgue differentiation theorem				L
03	Uncountability of the continuum				L
26	Intermediate value theorem				L
52	Carathéodory's theorem				L
20	Jordan–Hölder theorem				L
26	Heine–Borel theorem				L
28	Vitali theorem				X
28	Carathéodory's theorem				L
05	Binomial theorem				L
11	Wilson's theorem				L
20	Orbit-stabilizer theorem				L
11	Ostrowski's theorem				L
15	Rank–nullity theorem				L
26	Abel's theorem				L
28	Vitali covering theorem				L
91	Arrow's impossibility theorem				X
60	Kolmogorov extension theorem				X
05	Kruskal–Katona theorem				L
11	Mahler's theorem				L
16	Lattice theorem				L
15	Dimension theorem for vector spaces				L
46	Hilbert projection theorem				L
30	Hadamard three-lines theorem				L
06	Kleene fixed-point theorem				L
43	Fourier inversion theorem				L
68	Akra–Bazzi theorem				L
68	Myhill–Nerode theorem				L
30	Phragmén–Lindelöf theorem				L
51	Ptolemy's theorem				L
26	Bolzano–Weierstrass theorem				L
05	Four functions theorem				L
26	Stirling's theorem				L
11	Quadratic reciprocity theorem				L
03	Cantor's theorem				L
12	Solutions of a general quartic equation				L
03	Ax–Grothendieck theorem				L
18	Beck's monadicity theorem				L
20	Lagrange's theorem				L
11	Corners theorem				L
34	Picard–Lindelöf theorem				L
05	Hall's marriage theorem				L
46	Banach–Alaoglu theorem				L
26	Fatou–Lebesgue theorem				L
11	Dirichlet's theorem on arithmetic progressions				L
05	Friendship theorem				L
13	Vieta's formulas				L
30	Liouville's theorem				L
26	Dini's theorem				L
06	Knaster–Tarski theorem				L
05	Multinomial theorem				L
11	Bertrand's postulate				L
52	Krein–Milman theorem				L
13	Hilbert's basis theorem				L
15	Cayley–Hamilton theorem				L
12	Abel–Ruffini theorem				L
11	Fundamental theorem of arithmetic				L
46	Marcinkiewicz theorem				X
30	Mellin inversion theorem				L
11	Erdős–Ginzburg–Ziv theorem				L
05	Erdős–Ko–Rado theorem				L
12	Chevalley–Warning theorem				L
55	Whitney–Graustein Theorem				X
28	Schroeder–Bernstein theorem for measurable spaces				L
12	Schwartz–Zippel theorem				L
51	Sylvester–Gallai theorem				X
26	Extreme value theorem				L
11	Lagrange's four-square theorem				L
05	Van der Waerden's theorem				L
51	Heine–Cantor theorem				L
16	Artin–Wedderburn theorem				L
16	Structure theorem for finitely generated modules over a principal ideal domain				L
26	Basel problem				L
30	Cauchy integral theorem				L
05	Theorem on friends and strangers				X
54	Lebesgue's density theorem				L
26	Implicit function theorem				L
11	Solutions to Pell's equation				L
46	Hahn–Banach theorem				L
11	Fermat's theorem on sums of two squares				L
05	Ramsey's theorem				X
26	Inverse function theorem				L
46	Stone–Weierstrass theorem				L
13	Wedderburn's little theorem				L
46	Open mapping theorem				L
05	Kneser's theorem				X
30	Open mapping theorem				L
52	Erdős–Szekeres theorem				L
35	Lax–Milgram theorem				L