-
mathlib4 Public
Forked from leanprover-community/mathlib4The math library of Lean 4
Lean Apache License 2.0 UpdatedNov 1, 2025 -
-
lean4 Public
Forked from leanprover/lean4Lean 4 programming language and theorem prover
Lean Apache License 2.0 UpdatedOct 22, 2025 -
verso Public
Forked from leanprover/versoLean documentation authoring tool
JavaScript Apache License 2.0 UpdatedOct 14, 2025 -
HighlyAbundant Public
Formalisations relating to https://mathoverflow.net/q/501066/117945
-
-
AharoniKorman Public
Disproof of the Aharoni–Korman conjecture
-
ABC-Exceptions Public
Exceptions to the ABC conjecture in Lean
-
-
Course notes for Formalising Mathematics 2025
-
lean-action Public
Forked from leanprover/lean-actionGitHub action for standard CI in Lean projects
Shell Apache License 2.0 UpdatedJul 1, 2025 -
FLT Public
Forked from ImperialCollegeLondon/FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
Lean Apache License 2.0 UpdatedJun 1, 2025 -
doc-gen4 Public
Forked from leanprover/doc-gen4Document Generator for Lean 4
Lean Apache License 2.0 UpdatedMay 24, 2025 -
docs Public
Forked from github/docsThe open-source repo for docs.github.com
TypeScript Creative Commons Attribution 4.0 International UpdatedMay 20, 2025 -
GlimpseOfLean Public
Forked from PatrickMassot/GlimpseOfLeanAn introduction to theorem proving in Lean for the impatient.
Lean Apache License 2.0 UpdatedApr 24, 2025 -
batteries Public
Forked from leanprover-community/batteriesStandard Library for Lean 4
Lean Apache License 2.0 UpdatedApr 7, 2025 -
DividedPowers4 Public
Forked from AntoineChambert-Loir/DividedPowers4DividedPowers in Lean / Mathlib 4
Lean UpdatedApr 6, 2025 -
lean4web Public
Forked from leanprover-community/lean4webThe Lean 4 web editor
TypeScript Apache License 2.0 UpdatedFeb 25, 2025 -
reference-manual Public
Forked from leanprover/reference-manualThe Lean reference manual
JavaScript Apache License 2.0 UpdatedFeb 19, 2025 -
LeanProject Public template
Forked from pitmonticone/LeanProjectTemplate for blueprint-driven formalization projects in Lean.
Python Apache License 2.0 UpdatedOct 11, 2024 -
equational_theories Public
Forked from teorth/equational_theoriesA project to map out the relations between different equational theories of Magmas.
Lean Apache License 2.0 UpdatedOct 10, 2024 -
-
mathematics_in_lean_source Public
Forked from avigad/mathematics_in_lean_sourceSource code for the Mathematics in Lean tutorial.
Lean UpdatedSep 9, 2024 -
-
carleson Public
Forked from fpvandoorn/carlesonA formalized proof of Carleson's theorem in Lean
TeX Apache License 2.0 UpdatedJun 23, 2024 -
-
maths-notes Public
Lecture notes from Cambridge maths
-
linear-base Public
Forked from tweag/linear-baseStandard library for linear types in Haskell.
Haskell MIT License UpdatedDec 4, 2023 -
-
exponential-ramsey Public
A formal proof of an exponentially better upper bound on Ramsey numbers
{{ message }}