Revision #3449 → #4001 · back to history
modifiedIrrationality proof of the Pythagoreans3abe5d94b821
| Field | From #3449 | To #4001 |
|---|
| note | The classical Pythagorean result that √2 is irrational is stated directly as `irrational_sqrt_two`. | Verified: the classical Pythagorean result that √2 is irrational is stated directly as `irrational_sqrt_two` in Mathlib.NumberTheory.Real.Irrational. |
modifiedCantor's theorem on uncountable sets1f0c2c779250
| Field | From #3449 | To #4001 |
|---|
| note | Cantor's diagonal result that no function `α → Set α` is surjective—the foundational theorem of his theory of infinite sets—is `Function.cantor_surjective`; the cardinal form is `Cardinal.cantor`. | Verified: Cantor's diagonal result that no function `α → Set α` is surjective is `Function.cantor_surjective` in Mathlib.Logic.Function.Basic. |
modifiedRussell's paradoxbab8a0176b3b
| Field | From #3449 | To #4001 |
|---|
| note | The naive-set-theoretic Russell paradox is implicit in Lean's type-theoretic foundation (the set of all sets that do not contain themselves cannot be formed) but is not stated as a named declaration in Mathlib. | The naive-set-theoretic Russell paradox is implicit in Lean's type-theoretic foundation but is not stated as a named declaration in Mathlib. |
modifiedGödel's incompleteness theoremscab258531e8f
| Field | From #3449 | To #4001 |
|---|
| note | Gödel's first and second incompleteness theorems are not formalized in Mathlib; a separate project (FormalizingMathematics / Paulson's Isabelle work, and a Lean effort by Shing Tak Lam) exists outside Mathlib. | Gödel's first and second incompleteness theorems are not formalized in Mathlib. |
modifiedCategory theory4350fff018a4
| Field | From #3449 | To #4001 |
|---|
| note | The foundational notion of a category is formalized as `CategoryTheory.Category`, with an extensive library on functors, natural transformations, limits, and adjunctions built on top. | Verified: `CategoryTheory.Category` is defined at Mathlib/CategoryTheory/Category/Basic.lean:235, with an extensive library built on top. |
modifiedCommutative ring (vs non-commutative ring)e6cbb9828f8e
| Field | From #3449 | To #4001 |
|---|
| note | Magid's ring-theory analogy refers to the standard distinction between `Ring` (not-necessarily-commutative) and `CommRing` (commutative); both are core algebraic typeclasses in Mathlib. | Verified: `CommRing` is defined in Mathlib.Algebra.Ring.Defs alongside `Ring`. |
modifiedConic sections1d32509e9b5e
| Field | From #3449 | To #4001 |
|---|
| note | Mathlib has the individual conics (circle, ellipse, parabola, hyperbola) treated piecemeal via quadratic forms and affine geometry, but no unified Apollonian theory of conic sections as plane sections of a cone. | Mathlib has the individual conics (circle, ellipse, parabola, hyperbola) treated piecemeal, but no unified Apollonian theory of conic sections as plane sections of a cone. |
modifiedLanglands programc2dce9b8e83f
| Field | From #3449 | To #4001 |
|---|
| note | Neither the classical nor the geometric Langlands correspondence is formalized in Mathlib; pieces of the prerequisite automorphic-forms and Galois-representations infrastructure exist but no Langlands-style functoriality statement. | Neither the classical nor the geometric Langlands correspondence is formalized in Mathlib. |
modifiedTopology (topological space)a7418f7a6f03
| Field | From #3449 | To #4001 |
|---|
| note | Point-set topology, the 20th-century formalization referenced here, is captured by the `TopologicalSpace` typeclass with a vast Mathlib development on continuity, compactness, and connectedness. | Verified: the `TopologicalSpace` typeclass is defined in Mathlib.Topology.Defs.Basic. |
modifiedGroup theory04b98ad7e7e8
| Field | From #3449 | To #4001 |
|---|
| note | The `Group` typeclass is a core algebraic structure in Mathlib, with a large body of finite/abelian/Lie group theory built on it. | Verified: `class Group` is at Mathlib/Algebra/Group/Defs.lean:33. |
modifiedMatrix theoryd54d3fa60d3b
| Field | From #3449 | To #4001 |
|---|
| note | Matrices over a semiring are formalized as `Matrix m n α` (in `Mathlib.LinearAlgebra.Matrix.Defs`), with a rich Mathlib API covering determinants, invertibility, eigenvalues, and spectral theory. | Verified: `def Matrix` is at Mathlib/LinearAlgebra/Matrix/Defs.lean:57. |
modifiedFunctional analysis2b6294fd5671
| Field | From #3449 | To #4001 |
|---|
| note | Functional analysis is a mature Mathlib area (normed and Banach spaces, Hilbert spaces, operator theory, Hahn–Banach); `NormedSpace` (in `Mathlib.Analysis.Normed.Module.Basic`) is a representative foundational typeclass. | Functional analysis is a mature Mathlib area; `NormedSpace` in Mathlib.Analysis.Normed.Module.Basic is a representative foundational typeclass. |
modifiedDynamical systemsdfa950dc8c02
| Field | From #3449 | To #4001 |
|---|
| note | Mathlib's `Dynamics` folder covers fixed points, periodic points, ergodic theory, and topological dynamics; `Function.IsFixedPt` (defined in `Mathlib.Logic.Function.Defs`) is a representative foundational declaration. | Verified: `Function.IsFixedPt` is at Mathlib/Logic/Function/Defs.lean:214, with Mathlib's `Dynamics` folder covering periodic points, ergodic theory, and topological dynamics. |
modifiedNumber theorycb8cc892ad20
| Field | From #3449 | To #4001 |
|---|
| note | Number theory is a large Mathlib area; `Nat.Prime` (in `Mathlib.Data.Nat.Prime.Defs`) is a representative core declaration and the folder `Mathlib.NumberTheory` develops arithmetic, L-functions, and modular forms. | Number theory is a large Mathlib area; `Nat.Prime` in Mathlib.Data.Nat.Prime.Defs is a representative core declaration, and Mathlib.NumberTheory develops arithmetic, L-functions, and modular forms. |
modifiedAlgebraic geometrya308c2a67c88
| Field | From #3449 | To #4001 |
|---|
| note | Algebraic geometry in Mathlib is developed around the `AlgebraicGeometry.Scheme` structure and the wider `Mathlib.AlgebraicGeometry` folder covering sheaves, morphisms, and projective schemes. | Verified: algebraic geometry in Mathlib is developed around the `AlgebraicGeometry.Scheme` structure in Mathlib.AlgebraicGeometry.Scheme. |
addedStatistics4545e7405890
addedPolynomial and rational functions64b060645ad7
addedSet theory (foundation for curriculum)d272412dfc06
addedLean proof assistantd163a5108833