All tags
Catalogue tag

#lean4

Every repository in the public record carrying this tag — from its GitHub topics or the keywords its package registries publish. Health is measured under the same versioned methodology as the rest of the record.

13 records
Tagged “lean4”Ranked by health index
npm
72Goodhealth index
google-deepmind/formal-conjectures
A collection of formalized statements of conjectures in Lean.
Lean★ 1,053Jul 19, 2026
Apache-2.0Jul 19, 2026 · metrics 1.13.0
68Moderatehealth index
leanprover-community/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Lean★ 406Jul 17, 2026
Apache-2.0Jul 17, 2026 · metrics 1.13.0
68Moderatehealth index
leanprover/std4
The "batteries included" extended library for the Lean programming language and theorem prover
Lean★ 407Jul 18, 2026
Apache-2.0Jul 18, 2026 · metrics 1.13.0
npm
64Moderatehealth index
leanprover-community/proofwidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
Lean · TypeScript★ 216↓ 13/moJul 17, 2026
Apache-2.0Jul 17, 2026 · metrics 1.13.0
64Moderatehealth index
leanprover/doc-gen4
Document Generator for Lean 4
Lean · Python★ 161Jul 19, 2026
Apache-2.0Jul 19, 2026 · metrics 1.13.0
PyPI
60Moderatehealth index
AxiomMath/axiom-lean-engine
Lean evaluation and metaprogramming utilities for provers.
Python★ 137↓ 5,215/moJul 19, 2026
MITJul 19, 2026 · metrics 1.13.0
60Moderatehealth index
leanprover-community/aesop
White-box automation for Lean 4
Lean★ 380Jul 15, 2026
Apache-2.0Jul 15, 2026 · metrics 1.13.0
59Moderatehealth index
leanprover/lean4-cli
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
Lean★ 113Jul 17, 2026
MITJul 17, 2026 · metrics 1.13.0
57Moderatehealth index
leanprover-community/quote4
Intuitive, type-safe expression quotations for Lean 4.
Lean★ 111Jul 17, 2026
Apache-2.0Jul 17, 2026 · metrics 1.13.0
56Moderatehealth index
leanprover-community/import-graph
Tool to analyse the import structure of lean projects.
Lean · HTML★ 22Jul 17, 2026
Apache-2.0Jul 17, 2026 · metrics 1.13.0
51Moderatehealth index
dupuisf/bibtexquery
A simple command-line bibtex query utility written in Lean 4
Lean★ 11Jul 17, 2026
Apache-2.0Jul 17, 2026 · metrics 1.13.0
npm · PyPI
41At riskhealth index
sthamann/tfpt
Topological Fixed-Point Theory: a machine-checked discrete compiler for the Standard Model, α⁻¹, and cosmology from two axioms. Papers, verification suite (Python/Wolfram/Lean), experiments & website.
Python · TeX · TypeScript★ 715Jul 21, 2026
No licenseJul 21, 2026 · metrics 1.13.0