Ecosyste.ms: Repos
An open API service providing repository metadata for many open source software ecosystems.
GitHub topics: formal-mathematics
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Language: C++ - Size: 1.11 MB - Last synced: 1 day ago - Pushed: 2 days ago - Stars: 815 - Forks: 71
LogicalAtomist/principia
The Principia Rewrite
Language: TeX - Size: 10.2 MB - Last synced: 5 days ago - Pushed: 5 days ago - Stars: 199 - Forks: 5
pitmonticone/FLT Fork of ImperialCollegeLondon/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Language: TeX - Size: 29.8 MB - Last synced: 5 days ago - Pushed: 5 days ago - Stars: 1 - Forks: 1
pitmonticone/carleson Fork of fpvandoorn/carleson
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
Language: TeX - Size: 718 KB - Last synced: 10 days ago - Pushed: 10 days ago - Stars: 0 - Forks: 0
pitmonticone/FLT3 Fork of riccardobrasca/flt3
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
Language: TeX - Size: 550 KB - Last synced: 22 days ago - Pushed: 22 days ago - Stars: 1 - Forks: 1
leanprover-community/mathlib
Lean 3's obsolete mathematical components library: please use mathlib4
Language: Lean - Size: 213 MB - Last synced: 29 days ago - Pushed: about 1 month ago - Stars: 1,632 - Forks: 294
appliedfm/vstyle
A style guide for Coq
Size: 646 KB - Last synced: about 1 month ago - Pushed: over 2 years ago - Stars: 15 - Forks: 0
dtumad/lean-crypto-formalization
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
Language: Lean - Size: 2.13 MB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 7 - Forks: 0
eric-wieser/lean-matrix-cookbook
The matrix cookbook, proved in the Lean theorem prover
Language: Lean - Size: 199 KB - Last synced: about 1 month ago - Pushed: 4 months ago - Stars: 43 - Forks: 6
SReichelt/slate
The Slate Interactive Theorem Prover
Language: TypeScript - Size: 7.5 MB - Last synced: 2 months ago - Pushed: over 1 year ago - Stars: 23 - Forks: 1
FormalMathematicsLab/ICL_Course_FormalMathematics_2024 Fork of ImperialCollegeLondon/formalising-mathematics-2024
Repository hosting resources for the 2024 course in Formal Mathematics at @ImperialCollegeLondon taught by Kevin Buzzard (@kbuzzard).
Size: 317 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0
FormalMathematicsLab/UniRome_Workshop_Lean_2024 Fork of fpvandoorn/LeanInRome
Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
Size: 2.6 MB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0
eric-wieser/lean-graded-rings
A formalization of graded rings in Lean, corresponding to a CICM 2022 submission
Language: Lean - Size: 171 KB - Last synced: about 1 month ago - Pushed: over 1 year ago - Stars: 7 - Forks: 0
amka66/mai
mai: MAth Interpreter with standard foundations
Language: Prolog - Size: 133 KB - Last synced: 5 months ago - Pushed: over 1 year ago - Stars: 2 - Forks: 1
SReichelt/slate-hlm
HLM mathematical library for the Slate interactive theorem prover
Language: Shell - Size: 1.85 MB - Last synced: 10 months ago - Pushed: over 1 year ago - Stars: 2 - Forks: 1
bryangingechen/lean-matroids
matroids in lean
Language: Lean - Size: 58.6 KB - Last synced: about 2 months ago - Pushed: over 3 years ago - Stars: 3 - Forks: 1
adyavanapalli/natural-number-game-solutions
Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.
Size: 23.4 KB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 8 - Forks: 6
