Усі теги
Тег каталогу

#lean4

Усі репозиторії публічного реєстру з цим тегом — із тем GitHub або ключових слів, які публікують їхні реєстри пакетів. Здоров'я вимірюється за тією ж версіонованою методологією, що й решта реєстру.

23 записи
З тегом «lean4»Упорядковано за індексом здоров'я
—
94Винятковийіндекс здоров'я
leanprover-community/mathlib4
The math library of Lean 4
Lean★ 4 0649 вер. 2026 р.
Apache-2.09 вер. 2026 р. · метрики 2.10.0
npm
91Відміннийіндекс здоров'я
google-deepmind/formal-conjectures
A collection of formalized statements of conjectures in Lean.
Lean★ 1 25711 вер. 2026 р.
Apache-2.011 вер. 2026 р. · метрики 2.10.0
—
88Відміннийіндекс здоров'я
leanprover/lean4
Lean 4 programming language and theorem prover
Lean★ 9 23621 вер. 2026 р.
Apache-2.021 вер. 2026 р. · метрики 2.10.0
—
84Відміннийіндекс здоров'я
Verified-zkEVM/ArkLib
Formally Verified Arguments of Knowledge in Lean
Lean★ 34719 жовт. 2026 р.
Apache-2.019 жовт. 2026 р. · метрики 2.10.0
PyPI · RubyGems
83Відміннийіндекс здоров'я
fpvandoorn/carleson
A formalized proof of Carleson's theorem in Lean
Lean · TeX★ 11119 вер. 2026 р.
Apache-2.019 вер. 2026 р. · метрики 2.10.0
PyPI
81Відміннийіндекс здоров'я
oOo0oOo/lean-lsp-mcp
Lean Theorem Prover MCP
Python★ 530↓ 730.4K/міс19 жовт. 2026 р.
MIT19 жовт. 2026 р. · метрики 2.10.0
—
78Добрийіндекс здоров'я
leanprover-community/batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Lean★ 41811 вер. 2026 р.
Apache-2.011 вер. 2026 р. · метрики 2.10.0
npm
77Добрийіндекс здоров'я
leanprover-community/ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
Lean · TypeScript★ 2249 вер. 2026 р.
Apache-2.09 вер. 2026 р. · метрики 2.10.0
PyPI
73Добрийіндекс здоров'я
AxiomMath/axiom-lean-engine
Lean evaluation and metaprogramming utilities for provers.
Python★ 155↓ 3 421/міс11 вер. 2026 р.
MIT11 вер. 2026 р. · метрики 2.10.0
PyPI
73Добрийіндекс здоров'я
eic/EpsilonEridaniWorker
`epsiloneridani` keeps the EpsilonEridani Lean library moving, using a "bring your own agent" approach
Python★ 0↓ 2 023/міс10 жовт. 2026 р.
Apache-2.010 жовт. 2026 р. · метрики 2.10.0
npm
71Добрийіндекс здоров'я
TypeScript · JavaScript★ 15618 жовт. 2026 р.
Apache-2.018 жовт. 2026 р. · метрики 2.10.0
—
71Добрийіндекс здоров'я
leanprover/doc-gen4
Document Generator for Lean 4
Lean · Python★ 17011 вер. 2026 р.
Apache-2.011 вер. 2026 р. · метрики 2.10.0
PyPI
62Помірнийіндекс здоров'я
alerad/lean-runtime
Опис репозиторію не опубліковано.
Python★ 3↓ 412/міс19 жовт. 2026 р.
Apache-2.019 жовт. 2026 р. · метрики 2.10.0
—
62Помірнийіндекс здоров'я
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
C++★ 1 32216 вер. 2026 р.
MIT16 вер. 2026 р. · метрики 2.10.0
npm
62Помірнийіндекс здоров'я
midspiral/LemmaScript
verification toolchain for TypeScript (Tech Preview)
TypeScript★ 95↓ 8 230/міс13 вер. 2026 р.
MIT13 вер. 2026 р. · метрики 2.10.0
—
60Помірнийіндекс здоров'я
leanprover-community/aesop
White-box automation for Lean 4
Lean★ 4018 вер. 2026 р.
Apache-2.08 вер. 2026 р. · метрики 2.10.0
—
59Помірнийіндекс здоров'я
leanprover-community/import-graph
Tool to analyse the import structure of lean projects.
Lean · HTML★ 2610 вер. 2026 р.
Apache-2.010 вер. 2026 р. · метрики 2.10.0
—
59Помірнийіндекс здоров'я
leanprover/lean4-cli
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
Lean★ 12010 вер. 2026 р.
MIT10 вер. 2026 р. · метрики 2.10.0
—
57Помірнийіндекс здоров'я
leanprover-community/quote4
Intuitive, type-safe expression quotations for Lean 4.
Lean★ 11110 вер. 2026 р.
Apache-2.010 вер. 2026 р. · метрики 2.10.0
—
56Помірнийіндекс здоров'я
leanprover/Pantograph
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Lean★ 8120 вер. 2026 р.
Apache-2.020 вер. 2026 р. · метрики 2.10.0
npm
54Помірнийіндекс здоров'я
Paper-Proof/paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
TypeScript · Lean · CSS★ 54917 вер. 2026 р.
MIT17 вер. 2026 р. · метрики 2.10.0
—
48Слабкийіндекс здоров'я
dupuisf/BibtexQuery
A simple command-line bibtex query utility written in Lean 4
Lean★ 119 вер. 2026 р.
Apache-2.09 вер. 2026 р. · метрики 2.10.0
npm · PyPI
42Слабкийіндекс здоров'я
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★ 47312 вер. 2026 р.
Без ліцензії12 вер. 2026 р. · метрики 2.10.0