Foundations and type theory
Category theory 32 sources
| Source | Mathematical content |
|---|---|
| ImperialCollegeLondon/condensed-sets | Early condensed mathematics (Lean 3) |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| Paul-Lez/PersistentDecomp | Structure theorem for persistence modules |
| UniMath/UniMath | Univalent mathematics in Rocq/Coq; large formal category-theory corpus |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| Verified-zkEVM/PolyFun | Polynomial functors and interaction trees |
| YellPika/quasi-borel-spaces | Quasi-Borel spaces |
| YijunYuan/HarderNarasimhan | Harder–Narasimhan theory |
| agda/agda-categories | Category theory in Agda: limits, adjunctions, monoidal/enriched and higher categorical structures, fibrations and topoi |
| agda/cubical | Cubical type theory, homotopy type theory, and related mathematics in Agda |
| alexkeizer/QPFTypes | Quotients of polynomial functors; definitional (co)datatypes |
| awodey/joyal | Joyal's representation theorem |
| dagurtomas/LeanCondensed | Additional work on condensed mathematics by the author of Mathlib's condensed-mathematics library |
| dagurtomas/lean-solid | Solid abelian groups |
| emilyriehl/infinity-cosmos | ∞-cosmos theory over Mathlib's quasicategories; formal ∞-category theory |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| ivankobe/FactorizationSystems | Factorization systems |
| jwiegley/category-theory | Large axiom-free category-theory development: categories, functors, adjunctions, (co)limits, Kan constructions, monads/comonads and related structures |
| kim-em/lean-category-theory | Early category-theory development later incorporated into Mathlib |
| leanprover-community/lean-liquid | Liquid Tensor Experiment (Lean 3; condensed foundations now in Mathlib) |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mariovagomarzal/higher_category_theory | Higher-order categories after Cosme Llópez |
| mattrobball/BridgelandStability | Bridgeland stability conditions on triangulated categories |
| peabrainiac/lean-catdg | Categorical differential geometry |
| riccardobrasca/SDG | Synthetic differential geometry |
| rkirov/category-theory-in-context-lean | Lean companion to Riehl's Category Theory in Context |
| sinhp/HoTTLean | Groupoid and natural models of HoTT; semantics of type theory |
| sinhp/LeanFibredCategories | Fibred categories; this development is inactive and has been superseded by the corresponding Mathlib material |
| sinhp/Poly | Polynomial functors and locally cartesian closed categories |
| sinhp/displayed_categories | Displayed categories, including fibers, cartesian lifts, and Street fibrations |
| standardml/twelf | Twelf/LF examples and case studies: lambda calculi, Cartesian closed categories, Church–Rosser, cut elimination, Mini-ML, logic programming and metatheory |
| the1lab/1lab | Cross-linked HoTT reference in cubical Agda |
Higher category theory 7 sources
| Source | Mathematical content |
|---|---|
| UniMath/UniMath | Univalent mathematics in Rocq/Coq; large formal category-theory corpus |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| agda/agda-categories | Category theory in Agda: limits, adjunctions, monoidal/enriched and higher categorical structures, fibrations and topoi |
| agda/cubical | Cubical type theory, homotopy type theory, and related mathematics in Agda |
| emilyriehl/infinity-cosmos | ∞-cosmos theory over Mathlib's quasicategories; formal ∞-category theory |
| mariovagomarzal/higher_category_theory | Higher-order categories after Cosme Llópez |
| the1lab/1lab | Cross-linked HoTT reference in cubical Agda |
Logic 35 sources
| Source | Mathematical content |
|---|---|
| CakeML/candle | Formal definitions and proofs for Candle, a verified implementation of HOL Light developed within CakeML |
| FormalizedFormalLogic/Foundation | Mathematical logic: completeness, incompleteness, provability logic |
| FormalizedFormalLogic/Incompleteness | Incompleteness theorems; with FormalizedFormalLogic/ProvabilityLogic |
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| HOLMS-lib/HOLMS | HOL Light Library for Modal Systems: Kripke semantics, normal modal logics, labelled calculi, completeness and verified proof search |
| Mathias-Stout/Many-sorted-model-theory | Many-sorted logic toward the model theory of valued fields |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| PierreSenellart/descriptive-complexity | Descriptive complexity: NP-completeness via first-order reductions |
| SRI-CSL/PVS | PVS and its standard libraries, including the formal definitions used by NASALib |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| VTrelat/ZFLean | Set-theoretic development framework |
| acl2/acl2 | ACL2 Community Books: arithmetic, algebra, data structures, formal models of hardware and software, verified algorithms, and reusable definitions |
| agda/agda-stdlib | Agda standard library: algebraic structures, orders, relations, finite structures, and data types |
| avigad/lamr | Logic and Mechanized Reasoning textbook and code |
| codyroux/traat-lean | Selected lemmas from Term Rewriting and All That |
| digama0/mm0 | Metamath Zero/One formal specifications and examples, including arithmetic and metatheory |
| flypitch/flypitch | Independence of the continuum hypothesis (Lean 3) |
| iris/iris | Iris higher-order concurrent separation logic and program logic, including ghost-state constructions and proof automation |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/con-nf | Consistency of Quine's New Foundations |
| leanprover-community/iris-lean | Iris separation logic port |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| martinescardo/TypeTopology | Topology and logic from the univalent point of view, in Agda |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
| rocq-community/corn | Constructive mathematics library in Rocq/Coq |
| rocq-prover/rocq | Rocq core library: elementary logic, basic data types, equality, arithmetic foundations, and well-founded recursion |
| rocq-prover/stdlib | Rocq standard mathematical library: sets, lists, sorting, arithmetic, numbers, relations, and general-purpose definitions and theorems |
| seL4/l4v | Isabelle/HOL formal specifications and proofs for seL4, with reusable theories for machine words, state monads, separation logic, refinement, and program verification |
| standardml/twelf | Twelf/LF examples and case studies: lambda calculi, Cartesian closed categories, Church–Rosser, cut elimination, Mini-ML, logic programming and metatheory |
| sven-manthe/A-formalization-of-Borel-determinacy-in-Lean | Borel determinacy |
| teorth/equational_theories | Implication graph between magma equational laws |
| ufmg-smite/lean-smt | Automated proof tactics using satisfiability-modulo-theories solvers |
Set theory 13 sources
| Source | Mathematical content |
|---|---|
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| VTrelat/ZFLean | Set-theoretic development framework |
| YnirPaz/PCF-Theory | PCF theory |
| digama0/mm0 | Metamath Zero/One formal specifications and examples, including arithmetic and metatheory |
| flypitch/flypitch | Independence of the continuum hypothesis (Lean 3) |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| leanprover-community/con-nf | Consistency of Quine's New Foundations |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| rocq-prover/stdlib | Rocq standard mathematical library: sets, lists, sorting, arithmetic, numbers, relations, and general-purpose definitions and theorems |
| sven-manthe/A-formalization-of-Borel-determinacy-in-Lean | Borel determinacy |
Type theory 14 sources
| Source | Mathematical content |
|---|---|
| HoTT-Intro/Agda | Section-by-section Agda formalization of Rijke's Introduction to Homotopy Type Theory |
| HoTT/Coq-HoTT | Homotopy type theory in Rocq/Coq |
| UniMath/UniMath | Univalent mathematics in Rocq/Coq; large formal category-theory corpus |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| agda/cubical | Cubical type theory, homotopy type theory, and related mathematics in Agda |
| alexkeizer/QPFTypes | Quotients of polynomial functors; definitional (co)datatypes |
| gebner/hott3 | HoTT (Lean 3) |
| martinescardo/TypeTopology | Topology and logic from the univalent point of view, in Agda |
| rocq-prover/rocq | Rocq core library: elementary logic, basic data types, equality, arithmetic foundations, and well-founded recursion |
| rzrn/ground_zero | Homotopy type theory in Lean 4 |
| sinhp/HoTTLean | Groupoid and natural models of HoTT; semantics of type theory |
| sinhp/Poly | Polynomial functors and locally cartesian closed categories |
| standardml/twelf | Twelf/LF examples and case studies: lambda calculi, Cartesian closed categories, Church–Rosser, cut elimination, Mini-ML, logic programming and metatheory |
| the1lab/1lab | Cross-linked HoTT reference in cubical Agda |
Homotopy type theory 10 sources
| Source | Mathematical content |
|---|---|
| HoTT-Intro/Agda | Section-by-section Agda formalization of Rijke's Introduction to Homotopy Type Theory |
| HoTT/Coq-HoTT | Homotopy type theory in Rocq/Coq |
| UniMath/UniMath | Univalent mathematics in Rocq/Coq; large formal category-theory corpus |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| agda/cubical | Cubical type theory, homotopy type theory, and related mathematics in Agda |
| gebner/hott3 | HoTT (Lean 3) |
| martinescardo/TypeTopology | Topology and logic from the univalent point of view, in Agda |
| rzrn/ground_zero | Homotopy type theory in Lean 4 |
| sinhp/HoTTLean | Groupoid and natural models of HoTT; semantics of type theory |
| the1lab/1lab | Cross-linked HoTT reference in cubical Agda |
Modal type theory 2 sources
| Source | Mathematical content |
|---|---|
| HOLMS-lib/HOLMS | HOL Light Library for Modal Systems: Kripke semantics, normal modal logics, labelled calculi, completeness and verified proof search |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
Model theory 2 sources
| Source | Mathematical content |
|---|---|
| Mathias-Stout/Many-sorted-model-theory | Many-sorted logic toward the model theory of valued fields |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
Domain theory 3 sources
| Source | Mathematical content |
|---|---|
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| martinescardo/TypeTopology | Topology and logic from the univalent point of view, in Agda |
| zilberstein/domain-theory | Domain theory |
Order theory 5 sources
| Source | Mathematical content |
|---|---|
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| agda/agda-stdlib | Agda standard library: algebraic structures, orders, relations, finite structures, and data types |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| rocq-prover/stdlib | Rocq standard mathematical library: sets, lists, sorting, arithmetic, numbers, relations, and general-purpose definitions and theorems |
| zilberstein/domain-theory | Domain theory |
Computability 12 sources
| Source | Mathematical content |
|---|---|
| FormalizedFormalLogic/Foundation | Mathematical logic: completeness, incompleteness, provability logic |
| PierreSenellart/descriptive-complexity | Descriptive complexity: NP-completeness via first-order reductions |
| SamuelSchlesinger/sensitivity-conjecture | Huang's proof of the sensitivity conjecture |
| Timeroot/ComputableReal | Computable real numbers |
| acl2/acl2 | ACL2 Community Books: arithmetic, algebra, data structures, formal models of hardware and software, verified algorithms, and reusable definitions |
| avigad/lamr | Logic and Mechanized Reasoning textbook and code |
| ctchou/AutomataTheory | Automata theory |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| leanprover/cslib | Computer science library |
| madvorak/chomsky | Chomsky hierarchy and formal grammars |
| rocq-prover/rocq | Rocq core library: elementary logic, basic data types, equality, arithmetic foundations, and well-founded recursion |
| shetzl/autth | Automata theory |
Algebra
Universal algebra 3 sources
| Source | Mathematical content |
|---|---|
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| agda/agda-stdlib | Agda standard library: algebraic structures, orders, relations, finite structures, and data types |
| teorth/equational_theories | Implication graph between magma equational laws |
Finite algebraic structures 4 sources
| Source | Mathematical content |
|---|---|
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| agda/agda-stdlib | Agda standard library: algebraic structures, orders, relations, finite structures, and data types |
| iris/stdpp | General-purpose Rocq definitions for data structures, finite maps, and algebra, used by Iris and independently reusable |
| math-comp/math-comp | Mathematical Components: finite structures, algebra, finite group theory, field theory, matrices, and polynomials |
Group theory 17 sources
| Source | Mathematical content |
|---|---|
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| Luka-O/polya-enumeration-theorem | Pólya enumeration theorem |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| chrisflav/bruhat-tits | The Bruhat–Tits tree |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| math-comp/math-comp | Mathematical Components: finite structures, algebra, finite group theory, field theory, matrices, and polynomials |
| math-comp/odd-order | Feit–Thompson Odd Order Theorem and the supporting finite-group theory developed for its proof |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| npflueger/demazure | Demazure products |
| siddhartha-gadgil/Polylean | Group extensions and torsion-freeness with computational proofs |
| singerng/steinberg-formalization | Steinberg groups |
| wupr/order-p-q | Classification of groups of order pq |
| yawara/odd-order | Feit–Thompson odd order theorem in Lean 4, with the finite group theory library it required |
Finite group theory 7 sources
| Source | Mathematical content |
|---|---|
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| inQWIRE/QuantumLib | Reusable quantum-computing mathematics in Rocq/Coq: complex matrices, finite groups, subspaces, permutations, measurement and quantum operations |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| math-comp/math-comp | Mathematical Components: finite structures, algebra, finite group theory, field theory, matrices, and polynomials |
| math-comp/odd-order | Feit–Thompson Odd Order Theorem and the supporting finite-group theory developed for its proof |
| wupr/order-p-q | Classification of groups of order pq |
| yawara/odd-order | Feit–Thompson odd order theorem in Lean 4, with the finite group theory library it required |
Higher group theory 2 sources
| Source | Mathematical content |
|---|---|
| HoTT/Coq-HoTT | Homotopy type theory in Rocq/Coq |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
Ring theory 21 sources
| Source | Mathematical content |
|---|---|
| AntoineChambert-Loir/DividedPowers4 | Divided power structures and the divided-power algebra |
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| Hagb/lean-groebner | Gröbner bases, independent development |
| JJYYY-JJY/lean-normal-forms | Executable Hermite and Smith normal forms over Euclidean domains, with proofs relating them to Mathlib's definitions |
| JobPetrovcic/ArtinWedderburn | Artin–Wedderburn theorem |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| Verified-zkEVM/CompPoly | Computable polynomials |
| Whysoserioushah/BrauerGroup | Brauer groups |
| WuProver/groebner_proj | Gröbner basis theory; companions WuProver/MonomialOrderedPolynomial and WuProver/GroebnerTactic |
| girving/series | Power series arithmetic, with related formalizations of Böttcher series and verified Mandelbrot rendering |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| leanprover/sos | Sum-of-squares tactic for nonlinear real arithmetic |
| math-comp/math-comp | Mathematical Components: finite structures, algebra, finite group theory, field theory, matrices, and polynomials |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| pitmonticone/QuadraticIntegers | Rings of integers of quadratic fields |
| riccardobrasca/kaplanski4 | Kaplansky's criterion for unique factorization domains |
| singerng/steinberg-formalization | Steinberg groups |
Commutative algebra 16 sources
| Source | Mathematical content |
|---|---|
| AntoineChambert-Loir/DividedPowers4 | Divided power structures and the divided-power algebra |
| AxiomMath/fel-polynomial | Fel's conjecture on syzygies of numerical semigroups |
| BochaoKong/nullstellensatz | Local complex-analytic geometry: Rückert Nullstellensatz and foundations |
| CBirkbeck/uniform-sheafy-tate-domains-lean | Uniform sheafy Tate rings that are not stably uniform; Huber/Tate ring examples |
| Hagb/lean-groebner | Gröbner bases, independent development |
| ImperialCollegeLondon/FLT | Ongoing Fermat's Last Theorem formalization with substantial commutative algebra, dimension theory, and number theory |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| Whysoserioushah/BrauerGroup | Brauer groups |
| WuProver/groebner_proj | Gröbner basis theory; companions WuProver/MonomialOrderedPolynomial and WuProver/GroebnerTactic |
| acmepjz/lean-iwasawa | Iwasawa theory |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| leanprover-community/flt-regular | FLT for regular primes; cyclotomic-field material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mariainesdff/LocalClassFieldTheory | Local fields toward local class field theory, including discrete valuation rings, uniformizers, and completions at height-one primes |
| riccardobrasca/kaplanski4 | Kaplansky's criterion for unique factorization domains |
Field theory 9 sources
| Source | Mathematical content |
|---|---|
| Mathias-Stout/Many-sorted-model-theory | Many-sorted logic toward the model theory of valued fields |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| alok/lean-inf | Levi-Civita field for infinitesimal computation |
| kbuzzard/ClassFieldTheory | 2025 Clay Summer School project on class field theory |
| leanprover-community/flt-regular | FLT for regular primes; cyclotomic-field material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mariainesdff/HassePrinciple | Hilbert symbols and the Hasse–Minkowski invariant over general fields (Women in Numbers 7) |
| mariainesdff/LocalClassFieldTheory | Local fields toward local class field theory, including discrete valuation rings, uniformizers, and completions at height-one primes |
| math-comp/math-comp | Mathematical Components: finite structures, algebra, finite group theory, field theory, matrices, and polynomials |
Linear algebra 30 sources
| Source | Mathematical content |
|---|---|
| FredRaj3/SemicircleLaw | Wigner's semicircle law |
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| JJYYY-JJY/lean-normal-forms | Executable Hermite and Smith normal forms over Euclidean domains, with proofs relating them to Mathlib's definitions |
| JobPetrovcic/ArtinWedderburn | Artin–Wedderburn theorem |
| LieLean/LowDimSolvClassification | Classification of solvable Lie algebras of dimension at most three |
| LionSR/TNLean | Tensor networks: fundamental theorem of matrix product states, canonical forms |
| MichaelStollBayreuth/LegendreQF | Legendre's theorem on diagonal ternary quadratic forms; complete but defines no Hilbert symbol, Hasse invariant, or lattice notion |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| Paul-Lez/PersistentDecomp | Structure theorem for persistence modules |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| dududuguo/HighDimProb | High-dimensional probability, random matrices, concentration |
| eric-wieser/lean-matrix-cookbook | The Matrix Cookbook, proved |
| flyspeck/flyspeck | HOL Light formalization of the Kepler conjecture, together with the supporting geometry and analysis |
| inQWIRE/QuantumLib | Reusable quantum-computing mathematics in Rocq/Coq: complex matrices, finite groups, subspaces, permutations, measurement and quantum operations |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jonhanke/quadratic_forms_in_lean | Quadratic forms, with Cassels references and a small collection of definitions |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| leanprover/TensorLib | Verified tensor library |
| leanprover/hex-lll | Verified LLL lattice-basis reduction with a proved short-vector bound; a companion library proves correspondence with Mathlib's lattice definitions |
| lecopivo/LeanBLAS | BLAS bindings and specification |
| madvorak/duality | Linear-programming duality |
| mariainesdff/HassePrinciple | Hilbert symbols and the Hasse–Minkowski invariant over general fields (Women in Numbers 7) |
| math-comp/math-comp | Mathematical Components: finite structures, algebra, finite group theory, field theory, matrices, and polynomials |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
| oliver-butterley/SpectralThm | Spectral theorem |
| thefundamentaltheor3m/Sphere-Packing-Lean | Viazovska's dimension-8 sphere-packing theorem and the E8 lattice |
| thery/Selinger | Laurent Théry's formalization of Selinger's quantum-gate synthesis proof, combining number-theoretic and linear-algebraic definitions over Mathematical Components |
Representation theory 3 sources
| Source | Mathematical content |
|---|---|
| JobPetrovcic/ArtinWedderburn | Artin–Wedderburn theorem |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
Homological algebra 7 sources
| Source | Mathematical content |
|---|---|
| ImperialCollegeLondon/condensed-sets | Early condensed mathematics (Lean 3) |
| dagurtomas/LeanCondensed | Additional work on condensed mathematics by the author of Mathlib's condensed-mathematics library |
| dagurtomas/lean-solid | Solid abelian groups |
| kkytola/VirasoroProject | Witt algebra cohomology and the Virasoro algebra |
| leanprover-community/lean-liquid | Liquid Tensor Experiment (Lean 3; condensed foundations now in Mathlib) |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mattrobball/BridgelandStability | Bridgeland stability conditions on triangulated categories |
Lie theory 3 sources
| Source | Mathematical content |
|---|---|
| LieLean/LowDimSolvClassification | Classification of solvable Lie algebras of dimension at most three |
| kkytola/VirasoroProject | Witt algebra cohomology and the Virasoro algebra |
| leanprover-community/physlib | Formalized mathematical physics in Lean, including Riemannian and pseudo-Riemannian geometry, tensor calculus, relativity, distributions, Lie groups, crystal lattices, topological field theory, and lattice quantum… |
Quadratic forms 3 sources
| Source | Mathematical content |
|---|---|
| MichaelStollBayreuth/LegendreQF | Legendre's theorem on diagonal ternary quadratic forms; complete but defines no Hilbert symbol, Hasse invariant, or lattice notion |
| jonhanke/quadratic_forms_in_lean | Quadratic forms, with Cassels references and a small collection of definitions |
| mariainesdff/HassePrinciple | Hilbert symbols and the Hasse–Minkowski invariant over general fields (Women in Numbers 7) |
Lattices 2 sources
| Source | Mathematical content |
|---|---|
| leanprover/hex-lll | Verified LLL lattice-basis reduction with a proved short-vector bound; a companion library proves correspondence with Mathlib's lattice definitions |
| thefundamentaltheor3m/Sphere-Packing-Lean | Viazovska's dimension-8 sphere-packing theorem and the E8 lattice |
Number theory
Elementary number theory 16 sources
| Source | Mathematical content |
|---|---|
| CBirkbeck/AINTLIB | Atlas of formalized number theory |
| MichaelStollBayreuth/LegendreQF | Legendre's theorem on diagonal ternary quadratic forms; complete but defines no Hilbert symbol, Hasse invariant, or lattice notion |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| b-mehta/PrimeCert | Formal prime certificates |
| hanwenzhu/miller-rabin | Miller–Rabin primality test |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| riccardobrasca/flt3 | Fermat's Last Theorem for exponent 3 |
| rocq-prover/stdlib | Rocq standard mathematical library: sets, lists, sorting, arithmetic, numbers, relations, and general-purpose definitions and theorems |
| thery/Selinger | Laurent Théry's formalization of Selinger's quantum-gate synthesis proof, combining number-theoretic and linear-algebraic definitions over Mathematical Components |
| thery/coqprime | Number theory, elliptic curves, modular arithmetic, and primality certification |
| wwylele/PentagonalNumberTheorem | Euler's pentagonal number theorem |
Algebraic number theory 15 sources
| Source | Mathematical content |
|---|---|
| CBirkbeck/AINTLIB | Atlas of formalized number theory |
| ImperialCollegeLondon/FLT | Ongoing Fermat's Last Theorem formalization with substantial commutative algebra, dimension theory, and number theory |
| MichaelStollBayreuth/Heights | Theory of heights |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| acmepjz/lean-iwasawa | Iwasawa theory |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| kbuzzard/ClassFieldTheory | 2025 Clay Summer School project on class field theory |
| leanprover-community/flt-regular | FLT for regular primes; cyclotomic-field material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mariainesdff/HassePrinciple | Hilbert symbols and the Hasse–Minkowski invariant over general fields (Women in Numbers 7) |
| mariainesdff/LocalClassFieldTheory | Local fields toward local class field theory, including discrete valuation rings, uniformizers, and completions at height-one primes |
| pitmonticone/QuadraticIntegers | Rings of integers of quadratic fields |
| riccardobrasca/KummerCriterion | Kummer's criterion for regular primes |
| riccardobrasca/flt3 | Fermat's Last Theorem for exponent 3 |
| smmercuri/adele-ring_locally-compact | Local compactness of the adele ring of a number field |
Analytic number theory 11 sources
| Source | Mathematical content |
|---|---|
| AlexKontorovich/PrimeNumberTheoremAnd | Prime Number Theorem and related analytic number theory |
| CBirkbeck/AINTLIB | Atlas of formalized number theory |
| CBirkbeck/DirichletNonvanishing | Nonvanishing of Dirichlet L-functions |
| MichaelStollBayreuth/EulerProducts | Euler products and L-series |
| ahhwuhu/zeta_3_irrational | Irrationality of ζ(3) |
| amellendijk/selberg-sieve4 | The Selberg sieve |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| math-inc/strongpnt | Strong prime number theorem with the required complex analysis |
| teorth/expdb | Exponent-pair database for analytic number theory |
Arithmetic geometry 11 sources
| Source | Mathematical content |
|---|---|
| ANR-FALSE/PadicModForms | p-adic modular forms |
| CBirkbeck/ModularForms_Lean4 | Modular forms |
| ImperialCollegeLondon/FLT | Ongoing Fermat's Last Theorem formalization with substantial commutative algebra, dimension theory, and number theory |
| KisaraBlue/ec-tate-lean | Tate's algorithm for elliptic curves, executable |
| MichaelStollBayreuth/Heights | Theory of heights |
| b-mehta/ABC-Exceptions | Exceptions to the ABC conjecture |
| kckennylau/EllipticCurve | Toward a general definition of elliptic curves over schemes |
| leanprover-community/lean-perfectoid-spaces | Perfectoid spaces (Lean 3) |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| loefflerd/ModularFormDimensions | Finite-dimensionality of modular-form spaces |
| thery/coqprime | Number theory, elliptic curves, modular arithmetic, and primality certification |
p-adic number theory and geometry 9 sources
| Source | Mathematical content |
|---|---|
| ANR-FALSE/PadicModForms | p-adic modular forms |
| CBirkbeck/uniform-sheafy-tate-domains-lean | Uniform sheafy Tate rings that are not stably uniform; Huber/Tate ring examples |
| KisaraBlue/ec-tate-lean | Tate's algorithm for elliptic curves, executable |
| acmepjz/lean-iwasawa | Iwasawa theory |
| chrisflav/bruhat-tits | The Bruhat–Tits tree |
| kbuzzard/ClassFieldTheory | 2025 Clay Summer School project on class field theory |
| leanprover-community/lean-perfectoid-spaces | Perfectoid spaces (Lean 3) |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mariainesdff/LocalClassFieldTheory | Local fields toward local class field theory, including discrete valuation rings, uniformizers, and completions at height-one primes |
Modular forms 3 sources
| Source | Mathematical content |
|---|---|
| ANR-FALSE/PadicModForms | p-adic modular forms |
| CBirkbeck/ModularForms_Lean4 | Modular forms |
| loefflerd/ModularFormDimensions | Finite-dimensionality of modular-form spaces |
Elliptic curves 3 sources
| Source | Mathematical content |
|---|---|
| KisaraBlue/ec-tate-lean | Tate's algorithm for elliptic curves, executable |
| kckennylau/EllipticCurve | Toward a general definition of elliptic curves over schemes |
| thery/coqprime | Number theory, elliptic curves, modular arithmetic, and primality certification |
Geometry and topology
Algebraic geometry 16 sources
| Source | Mathematical content |
|---|---|
| AntoineChambert-Loir/DividedPowers4 | Divided power structures and the divided-power algebra |
| BochaoKong/nullstellensatz | Local complex-analytic geometry: Rückert Nullstellensatz and foundations |
| CBirkbeck/uniform-sheafy-tate-domains-lean | Uniform sheafy Tate rings that are not stably uniform; Huber/Tate ring examples |
| DhyeyMavani2003/chip-firing-with-lean | Chip-firing games and Riemann–Roch for graphs |
| GeoCoq/GeoCoq | Synthetic geometry from Tarski-style axioms, with Euclidean, Hilbert, parallel-postulate, and algebraic geometry developments |
| ImperialCollegeLondon/FLT | Ongoing Fermat's Last Theorem formalization with substantial commutative algebra, dimension theory, and number theory |
| MichaelStollBayreuth/Weights | Minimization of hypersurfaces (Elsenhans–Stoll) |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| Whysoserioushah/BrauerGroup | Brauer groups |
| YaelDillies/toric | Toric varieties over Mathlib's schemes |
| YijunYuan/HarderNarasimhan | Harder–Narasimhan theory |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| kckennylau/EllipticCurve | Toward a general definition of elliptic curves over schemes |
| leanprover-community/lean-perfectoid-spaces | Perfectoid spaces (Lean 3) |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mattrobball/BridgelandStability | Bridgeland stability conditions on triangulated categories |
Topology 17 sources
| Source | Mathematical content |
|---|---|
| AlexKontorovich/CoveringSpacesProject | Covering spaces and universal covers; overlaps the Tau Ceti universal-covers roadmap |
| Dominique-Lawson/Directed-Topology-Lean-4 | Directed topology |
| ImperialCollegeLondon/condensed-sets | Early condensed mathematics (Lean 3) |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| dagurtomas/LeanCondensed | Additional work on condensed mathematics by the author of Mathlib's condensed-mathematics library |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| leanprover-community/sphere-eversion | Sphere eversion via convex integration; h-principle |
| martinescardo/TypeTopology | Topology and logic from the univalent point of view, in Agda |
| math-comp/analysis | Real and classical analysis over Mathematical Components: topology, measure/integration, real numbers, sequences, and distributions |
| mccorvie/classification-of-surfaces | Classification of compact surfaces |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| rocq-community/corn | Constructive mathematics library in Rocq/Coq |
| smmercuri/adele-ring_locally-compact | Local compactness of the adele ring of a number field |
Algebraic topology 5 sources
| Source | Mathematical content |
|---|---|
| AlexKontorovich/CoveringSpacesProject | Covering spaces and universal covers; overlaps the Tau Ceti universal-covers roadmap |
| Paul-Lez/PersistentDecomp | Structure theorem for persistence modules |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| mccorvie/classification-of-surfaces | Classification of compact surfaces |
Homotopy theory 7 sources
| Source | Mathematical content |
|---|---|
| HoTT/Coq-HoTT | Homotopy type theory in Rocq/Coq |
| UniMath/UniMath | Univalent mathematics in Rocq/Coq; large formal category-theory corpus |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| agda/cubical | Cubical type theory, homotopy type theory, and related mathematics in Agda |
| emilyriehl/infinity-cosmos | ∞-cosmos theory over Mathlib's quasicategories; formal ∞-category theory |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| leanprover-community/sphere-eversion | Sphere eversion via convex integration; h-principle |
Differential geometry 9 sources
| Source | Mathematical content |
|---|---|
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| leanprover-community/physlib | Formalized mathematical physics in Lean, including Riemannian and pseudo-Riemannian geometry, tensor calculus, relativity, distributions, Lie groups, crystal lattices, topological field theory, and lattice quantum… |
| leanprover-community/sphere-eversion | Sphere eversion via convex integration; h-principle |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
| peabrainiac/lean-catdg | Categorical differential geometry |
| riccardobrasca/SDG | Synthetic differential geometry |
| urkud/SardMoreira | Moreira's version of Sard's theorem; with fpvandoorn/sard |
Synthetic geometry 2 sources
| Source | Mathematical content |
|---|---|
| GeoCoq/GeoCoq | Synthetic geometry from Tarski-style axioms, with Euclidean, Hilbert, parallel-postulate, and algebraic geometry developments |
| loganrjmurphy/LeanEuclid | Formal System E for Euclidean geometry, Book I of Euclid's Elements, and the UniGeo formalized problem corpus |
Discrete geometry 13 sources
| Source | Mathematical content |
|---|---|
| Antoine-dSG/frieze_patterns | Coxeter's frieze patterns |
| Jun2M/Main-theorem-of-polytopes | Main theorem of polytopes |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| YaelDillies/toric | Toric varieties over Mathlib's schemes |
| chrisflav/bruhat-tits | The Bruhat–Tits tree |
| dwrensha/Rupert.lean | The Rupert problem for convex polyhedra; with jcreedcmu/Noperthedron |
| flyspeck/flyspeck | HOL Light formalization of the Kepler conjecture, together with the supporting geometry and analysis |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| jsm28/AperiodicMonotilesLean | Formalization of the aperiodic monotiles known as the hat and spectre |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| rocq-community/fourcolor | Four Color Theorem, including the graph theory and real analysis needed for the proof |
| thefundamentaltheor3m/Sphere-Packing-Lean | Viazovska's dimension-8 sphere-packing theorem and the E8 lattice |
| vasnesterov/HadwigerNelson | Hadwiger–Nelson bounds |
Convex geometry 5 sources
| Source | Mathematical content |
|---|---|
| Jun2M/Main-theorem-of-polytopes | Main theorem of polytopes |
| dwrensha/Rupert.lean | The Rupert problem for convex polyhedra; with jcreedcmu/Noperthedron |
| flyspeck/flyspeck | HOL Light formalization of the Kepler conjecture, together with the supporting geometry and analysis |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| thefundamentaltheor3m/Sphere-Packing-Lean | Viazovska's dimension-8 sphere-packing theorem and the E8 lattice |
Analysis and probability
Real analysis 24 sources
| Source | Mathematical content |
|---|---|
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| Timeroot/ComputableReal | Computable real numbers |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| alerad/leancert | Verified interval arithmetic: bounds on exp, sin, cos; root finding |
| alok/lean-inf | Levi-Civita field for infinitesimal computation |
| flyspeck/flyspeck | HOL Light formalization of the Kepler conjecture, together with the supporting geometry and analysis |
| fpvandoorn/BonnAnalysis | Bonn collaborative analysis seminar (distributions, duality) |
| fpvandoorn/carleson | Carleson's theorem |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| leanprover/sos | Sum-of-squares tactic for nonlinear real arithmetic |
| lua-vr/pointwise-birkhoff | Pointwise Birkhoff ergodic theorem |
| math-comp/analysis | Real and classical analysis over Mathematical Components: topology, measure/integration, real numbers, sequences, and distributions |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
| rocq-community/corn | Constructive mathematics library in Rocq/Coq |
| scottnarmstrong/DeGiorgi | De Giorgi–Nash–Moser theory |
| teorth/analysis | Lean companion to Tao's Analysis I |
| uda-lab/leray-hopf | Leray–Hopf weak solutions of incompressible Navier–Stokes |
| urkud/SardMoreira | Moreira's version of Sard's theorem; with fpvandoorn/sard |
| weiran-sun/pde | PDE formalizations |
Complex analysis 16 sources
| Source | Mathematical content |
|---|---|
| AlexKontorovich/PrimeNumberTheoremAnd | Prime Number Theorem and related analytic number theory |
| BochaoKong/nullstellensatz | Local complex-analytic geometry: Rückert Nullstellensatz and foundations |
| CBirkbeck/DirichletNonvanishing | Nonvanishing of Dirichlet L-functions |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| girving/ray | Mandelbrot-set results |
| girving/series | Power series arithmetic, with related formalizations of Böttcher series and verified Mandelbrot rendering |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| kebekus/ProjectVD | Value distribution theory (Nevanlinna) |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| math-inc/strongpnt | Strong prime number theorem with the required complex analysis |
| metamath/set.mm | Metamath Proof Explorer and companion databases: ZFC mathematics plus intuitionistic set theory, NF, higher-order and quantum logic databases |
| samuelborza/IsTranscendentalPi | Transcendence of π |
| teorth/sendov | Sendov's conjecture work |
| vbeffara/RMT4 | The Riemann mapping theorem |
Functional analysis 11 sources
| Source | Mathematical content |
|---|---|
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| fpvandoorn/BonnAnalysis | Bonn collaborative analysis seminar (distributions, duality) |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| math-comp/analysis | Real and classical analysis over Mathematical Components: topology, measure/integration, real numbers, sequences, and distributions |
| mrdouglasny/OSforGFF | Gaussian free field in d=4 and the Osterwalder–Schrader axioms |
| oliver-butterley/SpectralThm | Spectral theorem |
| scottnarmstrong/DeGiorgi | De Giorgi–Nash–Moser theory |
| uda-lab/leray-hopf | Leray–Hopf weak solutions of incompressible Navier–Stokes |
| weiran-sun/pde | PDE formalizations |
Harmonic analysis 3 sources
| Source | Mathematical content |
|---|---|
| fpvandoorn/carleson | Carleson's theorem |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| roos-j/lean-booleanfun | Analysis of Boolean functions, including Arrow's theorem |
Measure theory 12 sources
| Source | Mathematical content |
|---|---|
| IBM/FormalML | General probability in Rocq/Coq, including sigma-algebras, expectation, conditional expectation and martingales, with applications to stochastic approximation and reinforcement learning |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| RemyDegenne/brownian-motion | Construction of Brownian motion; with RemyDegenne/kolmogorov_extension4 |
| YellPika/quasi-borel-spaces | Quasi-Borel spaces |
| cameronfreer/exchangeability | Exchangeability and three proofs of de Finetti's theorem |
| fpvandoorn/carleson | Carleson's theorem |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| lua-vr/pointwise-birkhoff | Pointwise Birkhoff ergodic theorem |
| math-comp/analysis | Real and classical analysis over Mathematical Components: topology, measure/integration, real numbers, sequences, and distributions |
Probability 21 sources
| Source | Mathematical content |
|---|---|
| FredRaj3/SemicircleLaw | Wigner's semicircle law |
| IBM/FormalML | General probability in Rocq/Coq, including sigma-algebras, expectation, conditional expectation and martingales, with applications to stochastic approximation and reinforcement learning |
| Lean-MoDS/StatsMLlib | Verified probability, statistics, and learning theory; with Robby955/FormalSLT |
| LeanMachineLearning/LML | Lean Machine Learning Library |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| RemyDegenne/brownian-motion | Construction of Brownian motion; with RemyDegenne/kolmogorov_extension4 |
| RemyDegenne/testing-lower-bounds | Information theory and hypothesis-testing bounds |
| YaelDillies/cam-combi | Cambridge Part II/III graph theory, combinatorics, extremal and probabilistic combinatorics |
| YellPika/quasi-borel-spaces | Quasi-Borel spaces |
| cameronfreer/exchangeability | Exchangeability and three proofs of de Finetti's theorem |
| dududuguo/HighDimProb | High-dimensional probability, random matrices, concentration |
| formal-applied-math/formal-mathfin | Mathematical finance: Black–Scholes, Itô calculus, FTAP, Girsanov |
| inQWIRE/QuantumLib | Reusable quantum-computing mathematics in Rocq/Coq: complex matrices, finite groups, subspaces, permutations, measurement and quantum operations |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jrh13/hol-light | HOL Light and its mathematical library: analysis, topology, geometry, algebra, number theory, and related foundational material |
| kkytola/ExtremeValueProject | Fisher–Tippett–Gnedenko theorem |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| math-comp/analysis | Real and classical analysis over Mathematical Components: topology, measure/integration, real numbers, sequences, and distributions |
| mrdouglasny/OSforGFF | Gaussian free field in d=4 and the Osterwalder–Schrader axioms |
| roos-j/lean-booleanfun | Analysis of Boolean functions, including Arrow's theorem |
Stochastic processes 4 sources
| Source | Mathematical content |
|---|---|
| IBM/FormalML | General probability in Rocq/Coq, including sigma-algebras, expectation, conditional expectation and martingales, with applications to stochastic approximation and reinforcement learning |
| RemyDegenne/brownian-motion | Construction of Brownian motion; with RemyDegenne/kolmogorov_extension4 |
| formal-applied-math/formal-mathfin | Mathematical finance: Black–Scholes, Itô calculus, FTAP, Girsanov |
| kkytola/ExtremeValueProject | Fisher–Tippett–Gnedenko theorem |
Metric spaces 3 sources
| Source | Mathematical content |
|---|---|
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| teorth/analysis | Lean companion to Tao's Analysis I |
Spectral theory 4 sources
| Source | Mathematical content |
|---|---|
| FredRaj3/SemicircleLaw | Wigner's semicircle law |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| oliver-butterley/SpectralThm | Spectral theorem |
Dynamical systems 4 sources
| Source | Mathematical content |
|---|---|
| girving/ray | Mandelbrot-set results |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| lua-vr/pointwise-birkhoff | Pointwise Birkhoff ergodic theorem |
Partial differential equations 3 sources
| Source | Mathematical content |
|---|---|
| scottnarmstrong/DeGiorgi | De Giorgi–Nash–Moser theory |
| uda-lab/leray-hopf | Leray–Hopf weak solutions of incompressible Navier–Stokes |
| weiran-sun/pde | PDE formalizations |
Statistics 4 sources
| Source | Mathematical content |
|---|---|
| IBM/FormalML | General probability in Rocq/Coq, including sigma-algebras, expectation, conditional expectation and martingales, with applications to stochastic approximation and reinforcement learning |
| Lean-MoDS/StatsMLlib | Verified probability, statistics, and learning theory; with Robby955/FormalSLT |
| LeanMachineLearning/LML | Lean Machine Learning Library |
| or4nge19/NeuralNetworks | Neural networks |
Information theory 1 source
| Source | Mathematical content |
|---|---|
| RemyDegenne/testing-lower-bounds | Information theory and hypothesis-testing bounds |
Financial mathematics 1 source
| Source | Mathematical content |
|---|---|
| formal-applied-math/formal-mathfin | Mathematical finance: Black–Scholes, Itô calculus, FTAP, Girsanov |
Combinatorics
Combinatorics 27 sources
| Source | Mathematical content |
|---|---|
| Antoine-dSG/frieze_patterns | Coxeter's frieze patterns |
| AxiomMath/fel-polynomial | Fel's conjecture on syzygies of numerical semigroups |
| CakeML/game-of-life | HOL4 formalization of Conway's Game of Life and verified compilation into Life circuits, including executable semantics and circuit definitions |
| DhyeyMavani2003/chip-firing-with-lean | Chip-firing games and Riemann–Roch for graphs |
| Jun2M/Main-theorem-of-polytopes | Main theorem of polytopes |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| SamuelSchlesinger/sensitivity-conjecture | Huang's proof of the sensitivity conjecture |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| YaelDillies/cam-combi | Cambridge Part II/III graph theory, combinatorics, extremal and probabilistic combinatorics |
| YaelDillies/toric | Toric varieties over Mathlib's schemes |
| agda/agda-stdlib | Agda standard library: algebraic structures, orders, relations, finite structures, and data types |
| b-mehta/AharoniKorman | Disproof of the Aharoni–Korman conjecture |
| celioboulay/expander-graphs | Expander graphs |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| isabelle-prover/mirror-isabelle | Isabelle/HOL libraries covering logic, sets, algebra, analysis, topology, number theory, probability, and foundational theories |
| jsm28/AperiodicMonotilesLean | Formalization of the aperiodic monotiles known as the hat and spectre |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| madvorak/vcsp | General-valued constraint satisfaction |
| math-comp/math-comp | Mathematical Components: finite structures, algebra, finite group theory, field theory, matrices, and polynomials |
| math-inc/FrontierMathOpen-Hypergraphs | Formalization of a FrontierMath open problem on hypergraphs |
| mitchell-horner/ErdosStoneSimonovitsKovariSosTuran | Erdős–Stone–Simonovits and Kővári–Sós–Turán theorems |
| npflueger/demazure | Demazure products |
| rocq-community/fourcolor | Four Color Theorem, including the graph theory and real analysis needed for the proof |
| roos-j/lean-booleanfun | Analysis of Boolean functions, including Arrow's theorem |
| teorth/equational_theories | Implication graph between magma equational laws |
| vihdzp/combinatorial-games | Combinatorial game theory |
| wwylele/PentagonalNumberTheorem | Euler's pentagonal number theorem |
Graph theory 12 sources
| Source | Mathematical content |
|---|---|
| DhyeyMavani2003/chip-firing-with-lean | Chip-firing games and Riemann–Roch for graphs |
| Ivan-Sergeyev/seymour | Seymour's decomposition theorem for regular matroids |
| Mizar Mathematical Library | Mizar Mathematical Library: a centrally maintained collection of formal definitions and proofs across mainstream mathematics |
| UniMath/agda-unimath | Univalent mathematics in Agda, including extensive category theory |
| YaelDillies/cam-combi | Cambridge Part II/III graph theory, combinatorics, extremal and probabilistic combinatorics |
| celioboulay/expander-graphs | Expander graphs |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| math-inc/FrontierMathOpen-Hypergraphs | Formalization of a FrontierMath open problem on hypergraphs |
| mitchell-horner/ErdosStoneSimonovitsKovariSosTuran | Erdős–Stone–Simonovits and Kővári–Sós–Turán theorems |
| rocq-community/fourcolor | Four Color Theorem, including the graph theory and real analysis needed for the proof |
| vasnesterov/HadwigerNelson | Hadwiger–Nelson bounds |
Matroid theory 3 sources
| Source | Mathematical content |
|---|---|
| Ivan-Sergeyev/seymour | Seymour's decomposition theorem for regular matroids |
| apnelson1/Matroid | Matroid theory over Mathlib |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
Enumerative combinatorics 2 sources
| Source | Mathematical content |
|---|---|
| Luka-O/polya-enumeration-theorem | Pólya enumeration theorem |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
Additive combinatorics 4 sources
| Source | Mathematical content |
|---|---|
| YaelDillies/apap | Kelley–Meka bound on Roth numbers |
| leanprover-community/add-combi | Mathlib's additive-combinatorics sublibrary |
| leanprover-community/mathlib4 | Large formal mathematics library covering algebra, number theory, topology, analysis, measure theory, geometry, combinatorics, and many other subjects |
| teorth/pfr | Polynomial Freiman–Ruzsa conjecture and related additive combinatorics |
Game theory 2 sources
| Source | Mathematical content |
|---|---|
| math-xmum/gametheory | Nash equilibrium via Scarf and Brouwer |
| vihdzp/combinatorial-games | Combinatorial game theory |
Computation and verification
Optimization 12 sources
| Source | Mathematical content |
|---|---|
| Lean-MoDS/StatsMLlib | Verified probability, statistics, and learning theory; with Robby955/FormalSLT |
| LeanMachineLearning/LML | Lean Machine Learning Library |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| leanprover/sos | Sum-of-squares tactic for nonlinear real arithmetic |
| lecopivo/SciLean | Scientific computing |
| madvorak/duality | Linear-programming duality |
| madvorak/vcsp | General-valued constraint satisfaction |
| math-xmum/gametheory | Nash equilibrium via Scarf and Brouwer |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
| optsuite/optlib | Optimization algorithms and convergence proofs |
| or4nge19/NeuralNetworks | Neural networks |
| verified-optimization/CvxLean | Convex optimization modeling |
Numerical analysis 6 sources
| Source | Mathematical content |
|---|---|
| alerad/leancert | Verified interval arithmetic: bounds on exp, sin, cos; root finding |
| girving/interval | Verified floating-point interval arithmetic |
| josephmckinsey/Flean | Floating-point numbers, replacing Mathlib.Data.FP; with Beneficial-AI-Foundation/FloatSpec |
| lecopivo/LeanBLAS | BLAS bindings and specification |
| lecopivo/SciLean | Scientific computing |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
Scientific computing 4 sources
| Source | Mathematical content |
|---|---|
| leanprover/TensorLib | Verified tensor library |
| lecopivo/SciLean | Scientific computing |
| or4nge19/NeuralNetworks | Neural networks |
| todbeibrot/Lean-Oscar | Interface between Lean 4 and the OSCAR computer-algebra system |
Quantum information 6 sources
| Source | Mathematical content |
|---|---|
| Hayata-Yamasaki-Group/lean-quantum | Quantum information and computation; with inQWIRE/quantumlib |
| LionSR/TNLean | Tensor networks: fundamental theorem of matrix product states, canonical forms |
| Timeroot/Lean-QuantumInfo | Quantum information theory |
| inQWIRE/QuantumLib | Reusable quantum-computing mathematics in Rocq/Coq: complex matrices, finite groups, subspaces, permutations, measurement and quantum operations |
| leanprover-community/physlib | Formalized mathematical physics in Lean, including Riemannian and pseudo-Riemannian geometry, tensor calculus, relativity, distributions, Lie groups, crystal lattices, topological field theory, and lattice quantum… |
| thery/Selinger | Laurent Théry's formalization of Selinger's quantum-gate synthesis proof, combining number-theoretic and linear-algebraic definitions over Mathematical Components |
Mathematical physics 3 sources
| Source | Mathematical content |
|---|---|
| LionSR/TNLean | Tensor networks: fundamental theorem of matrix product states, canonical forms |
| leanprover-community/physlib | Formalized mathematical physics in Lean, including Riemannian and pseudo-Riemannian geometry, tensor calculus, relativity, distributions, Lie groups, crystal lattices, topological field theory, and lattice quantum… |
| mrdouglasny/OSforGFF | Gaussian free field in d=4 and the Osterwalder–Schrader axioms |
Semantics of programming languages and systems 19 sources
| Source | Mathematical content |
|---|---|
| AbsInt/CompCert | Formal definitions of C and assembly semantics, memory models and compiler passes, plus the correctness proofs of CompCert |
| CakeML/cakeml | HOL4 definitions of CakeML syntax and semantics, compiler/intermediate languages, type systems and the verified compiler proofs |
| CakeML/candle | Formal definitions and proofs for Candle, a verified implementation of HOL Light developed within CakeML |
| CakeML/game-of-life | HOL4 formalization of Conway's Game of Life and verified compilation into Life circuits, including executable semantics and circuit definitions |
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| HOLMS-lib/HOLMS | HOL Light Library for Modal Systems: Kripke semantics, normal modal logics, labelled calculi, completeness and verified proof search |
| SRI-CSL/PVS | PVS and its standard libraries, including the formal definitions used by NASALib |
| Verified-zkEVM/PolyFun | Polynomial functors and interaction trees |
| acl2/acl2 | ACL2 Community Books: arithmetic, algebra, data structures, formal models of hardware and software, verified algorithms, and reusable definitions |
| codyroux/traat-lean | Selected lemmas from Term Rewriting and All That |
| formal-land/rocq-of-rust | Formal definitions of Rust types, traits, integer operations, and control flow in Rocq, used to verify Rust programs |
| iris/iris | Iris higher-order concurrent separation logic and program logic, including ghost-state constructions and proof automation |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| kth-step/HOL4P4 | HOL4 formal syntax, small-step semantics, type system, architecture models and symbolic execution for the P4 language |
| leanprover-community/iris-lean | Iris separation logic port |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
| seL4/l4v | Isabelle/HOL formal specifications and proofs for seL4, with reusable theories for machine words, state monads, separation logic, refinement, and program verification |
| standardml/twelf | Twelf/LF examples and case studies: lambda calculi, Cartesian closed categories, Church–Rosser, cut elimination, Mini-ML, logic programming and metatheory |
| uwplse/verdi | Formal models and proofs for distributed systems, including reusable definitions for verified distributed algorithms |
Programming languages 13 sources
| Source | Mathematical content |
|---|---|
| AbsInt/CompCert | Formal definitions of C and assembly semantics, memory models and compiler passes, plus the correctness proofs of CompCert |
| CakeML/cakeml | HOL4 definitions of CakeML syntax and semantics, compiler/intermediate languages, type systems and the verified compiler proofs |
| CakeML/candle | Formal definitions and proofs for Candle, a verified implementation of HOL Light developed within CakeML |
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| formal-land/rocq-of-rust | Formal definitions of Rust types, traits, integer operations, and control flow in Rocq, used to verify Rust programs |
| iris/iris | Iris higher-order concurrent separation logic and program logic, including ghost-state constructions and proof automation |
| iris/stdpp | General-purpose Rocq definitions for data structures, finite maps, and algebra, used by Iris and independently reusable |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| kth-step/HOL4P4 | HOL4 formal syntax, small-step semantics, type system, architecture models and symbolic execution for the P4 language |
| leanprover/cslib | Computer science library |
| seL4/l4v | Isabelle/HOL formal specifications and proofs for seL4, with reusable theories for machine words, state monads, separation logic, refinement, and program verification |
| standardml/twelf | Twelf/LF examples and case studies: lambda calculi, Cartesian closed categories, Church–Rosser, cut elimination, Mini-ML, logic programming and metatheory |
| uwplse/verdi | Formal models and proofs for distributed systems, including reusable definitions for verified distributed algorithms |
Program verification 28 sources
| Source | Mathematical content |
|---|---|
| AbsInt/CompCert | Formal definitions of C and assembly semantics, memory models and compiler passes, plus the correctness proofs of CompCert |
| CakeML/cakeml | HOL4 definitions of CakeML syntax and semantics, compiler/intermediate languages, type systems and the verified compiler proofs |
| CakeML/candle | Formal definitions and proofs for Candle, a verified implementation of HOL Light developed within CakeML |
| CakeML/game-of-life | HOL4 formalization of Conway's Game of Life and verified compilation into Life circuits, including executable semantics and circuit definitions |
| GasStationManager/ArtificialAlgorithms | Verified algorithms implemented and proved by AIs |
| HOL-Theorem-Prover/HOL | HOL4 libraries covering higher-order logic, algebra, analysis, semantics, and large formal developments |
| SRI-CSL/PVS | PVS and its standard libraries, including the formal definitions used by NASALib |
| acl2/acl2 | ACL2 Community Books: arithmetic, algebra, data structures, formal models of hardware and software, verified algorithms, and reusable definitions |
| alerad/leancert | Verified interval arithmetic: bounds on exp, sin, cos; root finding |
| astrainfinita/Algorithm | Verified efficient algorithms |
| b-mehta/PrimeCert | Formal prime certificates |
| digama0/mm0 | Metamath Zero/One formal specifications and examples, including arithmetic and metatheory |
| formal-land/rocq-of-rust | Formal definitions of Rust types, traits, integer operations, and control flow in Rocq, used to verify Rust programs |
| girving/interval | Verified floating-point interval arithmetic |
| hanwenzhu/miller-rabin | Miller–Rabin primality test |
| iris/iris | Iris higher-order concurrent separation logic and program logic, including ghost-state constructions and proof automation |
| iris/stdpp | General-purpose Rocq definitions for data structures, finite maps, and algebra, used by Iris and independently reusable |
| isabelle-prover/mirror-afp-devel | Archive of Formal Proofs (AFP): a large Isabelle library spanning pure mathematics, algorithms, semantics, verification, and scientific applications |
| josephmckinsey/Flean | Floating-point numbers, replacing Mathlib.Data.FP; with Beneficial-AI-Foundation/FloatSpec |
| kth-step/HOL4P4 | HOL4 formal syntax, small-step semantics, type system, architecture models and symbolic execution for the P4 language |
| leanprover-community/iris-lean | Iris separation logic port |
| leanprover/cslib | Computer science library |
| leanprover/hex-lll | Verified LLL lattice-basis reduction with a proved short-vector bound; a companion library proves correspondence with Mathlib's lattice definitions |
| nasa/pvslib | NASALib: PVS formalizations spanning algebra, analysis, geometry, numerical methods, decision procedures, and applications |
| seL4/l4v | Isabelle/HOL formal specifications and proofs for seL4, with reusable theories for machine words, state monads, separation logic, refinement, and program verification |
| thery/coqprime | Number theory, elliptic curves, modular arithmetic, and primality certification |
| ufmg-smite/lean-smt | Automated proof tactics using satisfiability-modulo-theories solvers |
| uwplse/verdi | Formal models and proofs for distributed systems, including reusable definitions for verified distributed algorithms |
Computer algebra 7 sources
| Source | Mathematical content |
|---|---|
| Hagb/lean-groebner | Gröbner bases, independent development |
| JJYYY-JJY/lean-normal-forms | Executable Hermite and Smith normal forms over Euclidean domains, with proofs relating them to Mathlib's definitions |
| Verified-zkEVM/CompPoly | Computable polynomials |
| WuProver/groebner_proj | Gröbner basis theory; companions WuProver/MonomialOrderedPolynomial and WuProver/GroebnerTactic |
| acl2/acl2 | ACL2 Community Books: arithmetic, algebra, data structures, formal models of hardware and software, verified algorithms, and reusable definitions |
| leanprover/hex-lll | Verified LLL lattice-basis reduction with a proved short-vector bound; a companion library proves correspondence with Mathlib's lattice definitions |
| todbeibrot/Lean-Oscar | Interface between Lean 4 and the OSCAR computer-algebra system |
Automata theory 3 sources
| Source | Mathematical content |
|---|---|
| ctchou/AutomataTheory | Automata theory |
| madvorak/chomsky | Chomsky hierarchy and formal grammars |
| shetzl/autth | Automata theory |
Formal language theory 1 source
| Source | Mathematical content |
|---|---|
| madvorak/chomsky | Chomsky hierarchy and formal grammars |