leanprover-community

All

78 repositories

queueboard
Public
Mathlib4 review and triage dashboard
Python
•
Apache License 2.0
•9•8•27•2•Updated Aug 5, 2025Aug 5, 2025
blog
Public
Source for the community blog
Python
•25•7•4•7•Updated Aug 5, 2025Aug 5, 2025
mathlib4-nightly-testing
Public
nightly-testing and lean-pr-testing branches of Mathlib
Lean
•
Apache License 2.0
•708•0•0•5•Updated Aug 5, 2025Aug 5, 2025
batteries
Public
The "batteries included" extended library for the Lean programming language and theorem prover
lean lean4
Lean
•
Apache License 2.0
•124•322•24•55•Updated Aug 5, 2025Aug 5, 2025
mathlib4
Public
The math library of Lean 4
lean4
Lean
•
Apache License 2.0
•708•2.2k•271•1.9k•Updated Aug 5, 2025Aug 5, 2025
mathlib-manual
Public
Lean
•
Apache License 2.0
•34•1•0•1•Updated Aug 5, 2025Aug 5, 2025
leanprover-community.github.io
Public
Hosts the website for mathlib and other Lean community infrastructure.
CSS
•
MIT License
•152•64•18•7•Updated Aug 5, 2025Aug 5, 2025
mathlib_stats
Public
Display gitstats output on the mathlib website
Python
•6•2•0•0•Updated Aug 5, 2025Aug 5, 2025
iris-lean
Public
Lean 4 port of Iris, a higher-order concurrent separation logic framework
Lean
•
Apache License 2.0
•14•109•19•13•Updated Aug 4, 2025Aug 4, 2025
sphere-eversion
Public
Formalization of the existence of sphere eversions
Lean
•
Apache License 2.0
•15•44•0•0•Updated Aug 2, 2025Aug 2, 2025
lean-release-tag
Public
Action that creates a Git tag when updating to a new Lean release.
Shell
•0•0•1•0•Updated Aug 2, 2025Aug 2, 2025
lean4game
Public
Server to host lean games.
react lean4
TypeScript
•
GNU General Public License v3.0
•56•299•96•13•Updated Jul 28, 2025Jul 28, 2025
import-graph
Public
Tool to analyse the import structure of lean projects.
lean4
Lean
•
Apache License 2.0
•12•14•2•1•Updated Jul 27, 2025Jul 27, 2025
lint-style-action
Public
Mathlib style linter
0•1•0•1•Updated Jul 24, 2025Jul 24, 2025
repl
Public
A simple REPL for Lean 4, returning information about errors and sorries.
Lean
•
Apache License 2.0
•56•150•24•17•Updated Jul 24, 2025Jul 24, 2025
ProofWidgets4
Public
Helper toolkit for creating your own Lean 4 UserWidgets
lean lean4 visualization
Lean
•
Apache License 2.0
•40•151•13•0•Updated Jul 24, 2025Jul 24, 2025
aesop
Public
White-box automation for Lean 4
lean4
Lean
•
Apache License 2.0
•35•287•37•1•Updated Jul 24, 2025Jul 24, 2025
plausible
Public
Lean
•
Apache License 2.0
•8•52•1•3•Updated Jul 24, 2025Jul 24, 2025
quote4
Public
Intuitive, type-safe expression quotations for Lean 4.
lean4
Lean
•
Apache License 2.0
•15•90•14•7•Updated Jul 24, 2025Jul 24, 2025
logic_and_proof
Public
TeX
•
Apache License 2.0
•3•12•3•5•Updated Jul 17, 2025Jul 17, 2025
flt-regular
Public
Fermat's Last Theorem for regular primes
Lean
•
Apache License 2.0
•3•61•0•0•Updated Jul 15, 2025Jul 15, 2025
lean4-mode
Public
Emacs major mode for Lean 4
emacs lean4
Emacs Lisp
•
Apache License 2.0
•34•100•23•5•Updated Jul 14, 2025Jul 14, 2025
lean-auto
Public
Experiments on automation for Lean
Lean
•
Apache License 2.0
•21•126•10•2•Updated Jul 12, 2025Jul 12, 2025
NNG4
Public
Natural Number Game
lean4
Lean
•
Apache License 2.0
•48•199•28•6•Updated Jul 11, 2025Jul 11, 2025
mathematics_in_lean
Public
The user home repository for the Mathematics in Lean tutorial.
HTML
•
Apache License 2.0
•273•391•0•0•Updated Jul 10, 2025Jul 10, 2025
docgen-action
Public
Action to generate Lean documentation pages
JavaScript
•1•1•2•0•Updated Jul 4, 2025Jul 4, 2025
mathlib-update-action
Public
Action for automatically updating to Mathlib releases
JavaScript
•
MIT License
•1•2•0•2•Updated Jul 3, 2025Jul 3, 2025
mathlib4_docs
Public
lean4
4•9•0•0•Updated Jul 3, 2025Jul 3, 2025
lean4web
Public
The Lean 4 web editor
lean4
TypeScript
•
Apache License 2.0
•35•100•7•3•Updated Jun 21, 2025Jun 21, 2025
azure-scripts
Public
scripts and cron jobs for Azure
Python
•5•1•0•0•Updated Jun 19, 2025Jun 19, 2025