5Developer Tools
28 entries
Documentation & Literate Programming
- Verso SlidesVerso genre for reveal.js slide decks with checked Lean code.leanprover/verso-slides
- SubVersoExtracts highlighted Lean code for use in Verso and other tools.leanprover/subverso
- mdgenGenerates Markdown files from Lean sources.Seasawher/mdgen
- LiterateLeanFiles that are valid Markdown and valid Lean at the same time, with no preprocessor.tani/literate-lean
- lean-slidesRenders reveal.js slides from Markdown comments inside the infoview.0art0/lean-slides
- LeanTeXDSL for writing LaTeX Beamer presentations in Lean.kiranandcode/LeanTeX
- versotreedocGenerates a Verso document skeleton that mirrors a source tree.richardlford/versotreedoc
- doc-verification-bridgeDocumentation tool that extracts verification relationships from Lean code.NicolasRouquette/doc-verification-bridge
- lean-i18nTranslate Lean projects with PO files.hhu-adam/lean-i18n
Formatting & Linting
- leanfmtStructure-preserving code formatter.duckki/leanfmt
- lean-fmtCode formatter and linter with editor and CI integration.jcreinhold/lean-fmt
- leanerLinter, formatter and whole-program dead-code eliminator.SrGaabriel/leaner
- lint-llm-proofsLinters for patterns common in LLM-generated proofs.jessealama/lint-llm-proofs
Analysis & Inspection
- import-graphAnalyze and visualize a package's import structure (
lake exe graph).leanprover-community/import-graph - jixiaStatic analysis tool that extracts declarations, dependency graphs and tactic states.frenzymath/jixia
- FlameTCFlame graphs for debugging type class synthesis performance.hargoniX/Flame
- leaffDiff tool for Lean environments.alexjbest/leaff
- lean4exportPlain-text export of declarations for external checkers and tools.leanprover/lean4export
- ast_exportExports Lean 4 ASTs.digama0/ast_export
- lean2sexpConverts
.oleanfiles to s-expressions.andrejbauer/lean2sexp - NodeGraphGenerates dependency graphs between declarations.adamtopaz/NodeGraph
- lean4-dep-auditTraces a constant's transitive dependencies down to axioms,
externs and their C sources.levzlotnik/lean4-dep-audit - Lean FuzzGrammar-based fuzzing for Lean DSLs, using parser tables extracted from the compiler.kiranandcode/lean-fuzz
Kernels & Proof Checking
- lean4checkerReplays an environment to check that the kernel accepts every declaration (archived).leanprover/lean4checker
- ComparatorChecks that a solution proves exactly the stated challenge theorem, using only allowed axioms.leanprover/comparator
- Lean Kernel ArenaTest suite and leaderboard for independent Lean kernel implementations (source).
- SafeVerifyRobustly checks submitted proofs and implementations against a reference.GasStationManager/SafeVerify
- axiom-auditAxiom allowlist check that fails CI on
sorry,native_decideor custom axioms.leanprover-community/axiom-audit