leanprover-community

Community-built infrastructure for the Lean (https://leanprover.github.io/) theorem prover

Pinned Repositories

aesop
White-box automation for Lean 4
Language:Lean214 9 6328
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Language:Lean253 16 62105
lean
Lean 3 Theorem Prover (community fork)
Language:C++435 28 20580
lean-liquid
💧 Liquid Tensor Experiment
Language:Lean181 14 7615
lean4-metaprogramming-book
Language:Lean225 9 3956
lean4game
Server to host lean games.
Language:TypeScript198 9 22835
mathematics_in_lean
The user home repository for the Mathematics in Lean tutorial.
Language:HTML275 14 0200
mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4
Language:Lean1.7k 53 362298
mathlib4
The math library of Lean 4
Language:Lean1.6k 39 419342
ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
Language:Lean116 8 2127

leanprover-community's Repositories

leanprover-community/mathlib4
The math library of Lean 4
Language:Lean1.6k 39 419342
leanprover-community/mathematics_in_lean
The user home repository for the Mathematics in Lean tutorial.
Language:HTML275 14 0200
leanprover-community/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Language:Lean253 16 62105
leanprover-community/lean4-metaprogramming-book
Language:Lean225 9 3956
leanprover-community/aesop
White-box automation for Lean 4
Language:Lean214 9 6328
leanprover-community/lean4game
Server to host lean games.
Language:TypeScript198 9 22835
leanprover-community/ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
Language:Lean116 8 2127
leanprover-community/NNG4
Natural Number Game
Language:Lean115 11 4835
leanprover-community/repl
A simple REPL for Lean 4, returning information about errors and sorries.
Language:Lean82 17 1823
leanprover-community/lean-auto
Experiments in automation for Lean
Language:Lean75 10 1812
leanprover-community/quote4
Intuitive, type-safe expression quotations for Lean 4.
Language:Lean75 6 2212
leanprover-community/lean4-mode
Emacs major mode for Lean 4
Language:Emacs Lisp70 6 3128
leanprover-community/iris-lean
Lean 4 port of Iris, a higher-order concurrent separation logic framework
Language:Lean69 26 36
leanprover-community/lean4web
The Lean 4 web editor
Language:TypeScript68 9 3719
leanprover-community/con-nf
A formal consistency proof of Quine's set theory New Foundations
Language:Lean66 17 246
leanprover-community/duper
Language:Lean55 10 68
leanprover-community/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
Language:CSS55 12 38123
leanprover-community/flt-regular
Fermat's Last Theorem for regular primes
Language:Lean52 17 883
leanprover-community/mathport
Mathport is a tool for porting Lean3 projects to Lean4
Language:Lean43 8 8515
leanprover-community/sphere-eversion
Formalization of the existence of sphere eversions
Language:Lean36 14 5210
leanprover-community/plausible
Language:Lean233
leanprover-community/doc-gen
Generate HTML documentation for mathlib and Lean
Language:Python21 11 5020
leanprover-community/mathlib3port
Synport output from mathport for mathlib3
Language:Lean11 17 05
leanprover-community/LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
Language:Lean93
leanprover-community/import-graph
Tool to analyse the import structure of lean projects.
Language:Lean8 7 25
leanprover-community/mathlib4_docs
8 19 12
leanprover-community/blog
Source for the community blog
Language:Python6 17 1221
leanprover-community/logic_and_proof
Language:TeX62
leanprover-community/lean3port
Stub for downloading mathport artifacts for Lean 3
Language:Lean1 16 04
leanprover-community/mathlib_stats
Display gitstats output on the mathlib website
Language:Python1 10 45