Owner

leanprover

36 indexed repositories · View on GitHub

lean4
Lean 4 programming language and theorem prover

Lean · 9499 stars
cslib
The Lean Computer Science Library (CSLib)

Lean · 746 stars
elan
The Lean version manager

Rust · 655 stars
verso
Lean documentation authoring tool

Lean · 394 stars
vscode-lean4
VS Code extension for the Lean 4 programming language and theorem prover

TypeScript · 314 stars
theorem_proving_in_lean4
Theorem Proving in Lean 4

Lean · 277 stars
comparator

Lean · 240 stars
fp-lean
Functional Programming in Lean

Lean · 201 stars
doc-gen4
Document Generator for Lean 4

Lean · 174 stars
reference-manual
The Lean reference manual

Lean · 133 stars
lean4-cli
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.

Lean · 123 stars
SampCert
SampCert : Verified Differential Privacy

Lean · 105 stars
leansqlite
SQLite bindings for Lean

C · 53 stars
reservoir
Package registry for Lean/Lake.

Vue · 51 stars
TensorLib
A verified tensor library in Lean

Lean · 50 stars
lean-eval
Comparator-based Lean formal mathematics eval

Lean · 48 stars
lean-action
GitHub action for standard CI in Lean projects

Shell · 47 stars
lean4export
Plain-text declaration export for Lean 4

Lean · 45 stars
verso-templates
Templates for getting started with Verso

Lean · 40 stars
lean-beam
Claude/Codex skill and local workflow layer for efficient interaction with Lean 4 and Monte-Carlo Tree Search.

Lean · 37 stars
16 more repositories live on View on GitHub

Beginner friendly Everything

Open All

Issues somebody may already be working on are listed last. List everything by date

Boxed scalar closed terms are initialized eagerly at module initialization, so code in branches that are never taken runs before `main`
Open
- Is something wrong?
bug

Difficulty 5/5 Over a week Newbie friendliness 35/100

leanprover/lean4#15746 · Opened Oct 17, 2026

Maintainers usually reply within 1 day
How do I use/work on Boole?
Open
- Is something wrong?
Difficulty 1/5 Under an hour Newbie friendliness 28/100

leanprover/cslib#1144 · Opened Oct 17, 2026

Maintainers usually reply within 1 day
[Submission] Axiom Prover (Axiom Math)
Open
- Is something wrong?
Difficulty 1/5 Under an hour Newbie friendliness 45/100

leanprover/lean-eval-submissions#2145 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
segfault @[try_suggestion] accepts a suggester whose type gained section variables in a mutual block
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 48/100

leanprover/lean4#15744 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
`mkValueTypeClosure` type-checks closed terms when the local context has a let
Open
- Is something wrong?
bug

leanprover/lean4#15742 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
View other user's projects I have accessed
Open
- Is something wrong?
Difficulty 3/5 1-2 days Newbie friendliness 55/100

leanprover/lean-workbench#184 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
View/sort a user's projects by "last accessed" date
Open
- Is something wrong?
Difficulty 5/5 Over a week Newbie friendliness 35/100

leanprover/lean-workbench#183 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
building 4.35 now requires git checkout for lean4lean
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 45/100

leanprover/lean4#15741 · 4 comments · Opened Oct 16, 2026

Maintainers usually reply within 1 day
Please index Volland/lean-elpi
Open
- Is something wrong?
Difficulty 2/5 Under an hour Newbie friendliness 15/100

leanprover/reservoir#126 · Opened Oct 16, 2026
Equation lemmas fail to generate for structural recursion through `match` on the decreasing argument and a value bound by a monadic bind
Open
- Is something wrong?
Difficulty 5/5 Over a week Newbie friendliness 12/100

leanprover/lean4#15735 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
vcgen: a spec whose argument contains a pattern-matching lambda does not apply to the same program elaborated in another module
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 18/100

leanprover/lean4#15734 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
vcgen: a callee spec's argument fixed only by its precondition stays a metavariable
Open
- Is something wrong?
Difficulty 5/5 Over a week Newbie friendliness 18/100

leanprover/lean4#15733 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
vcgen: spec not applicable when a program argument is a projection `(mk e).env` that reduces to the spec's argument
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/lean4#15732 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
vcgen: no spec found for a call through a structure projection `ops.op x` with `ops` a concrete instance
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 30/100

leanprover/lean4#15731 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
vcgen: "Failed to apply split rule" for an over-applied `ite`, `(if c then f else g) x`
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 25/100

leanprover/lean4#15730 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
vcgen: an equation in the spec list whose left-hand side is an `ite` program is not used; the `ite` is split first
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/lean4#15729 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
vcgen: no `f.eq_def` fallback for a recursive function whose equation lemmas are conditional ("No spec found")
Open
- Is something wrong?
Difficulty 5/5 Over a week Newbie friendliness 15/100

leanprover/lean4#15728 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
`grind`: kernel rejects a proof that puts a `Vector Nat n` atom into an `RArray Nat`
Open
- Is something wrong?
bug

Difficulty 5/5 Over a week Newbie friendliness 15/100

leanprover/lean4#15726 · Opened Oct 16, 2026

Maintainers usually reply within 1 day
`grind`: kernel error with equations between constant functions
Open
- Is something wrong?
bug

Difficulty 5/5 Over a week Newbie friendliness 15/100

leanprover/lean4#15721 · Opened Oct 15, 2026

Maintainers usually reply within 1 day
Unused untyped `variable` declaration breaks `deriving DecidableEq`
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 22/100

leanprover/lean4#15720 · Opened Oct 15, 2026

Maintainers usually reply within 1 day
`vcgen frames` fails on types with abbreviation
Open
- Is something wrong?
bug

Difficulty 5/5 Over a week Newbie friendliness 15/100

leanprover/lean4#15713 · Opened Oct 15, 2026

Maintainers usually reply within 1 day
`grind`: kernel error because `abstractGroundMismatches?` passes the abstracted terms in reverse order
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/lean4#15700 · Opened Oct 15, 2026

Maintainers usually reply within 1 day
`lia`: kernel error in `eq_def_struct` with a dependent `Int` field (regression)
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 22/100

leanprover/lean4#15699 · Opened Oct 15, 2026

Maintainers usually reply within 1 day
grind: hypothesis treated as a match condition fails depending on hypothesis order (nested constructor pattern)
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 12/100

leanprover/lean4#15697 · 1 comment · 1 reaction · Opened Oct 14, 2026

Maintainers usually reply within 1 day
Manual-affecting error with linter output
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/subverso#245 · Opened Oct 14, 2026
autoImplicit auto-binds a name that collides with an existing out-of-scope declaration with only an editor inlay hint, no CLI/batch-visible diagnostic
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/lean4#15694 · Opened Oct 14, 2026

Maintainers usually reply within 1 day
`IO.appPath` fails when `/proc` belongs to another PID namespace
Open
- Is something wrong?
bug

Difficulty 2/5 1-3 hours Newbie friendliness 72/100

leanprover/lean4#15692 · 3 reactions · Opened Oct 14, 2026

Maintainers usually reply within 1 day
`vcgen`: unhelpful errors when migrating a `Std.Do` proof from `mvcgen`
Open
- Is something wrong?
bug

Difficulty 3/5 Half a day Newbie friendliness 62/100

leanprover/lean4#15691 · 2 comments · Opened Oct 14, 2026

Maintainers usually reply within 1 day
Kernel check slows down quadratically for `Nat` that are multiples of `2^64`
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 22/100

leanprover/lean4#15686 · 2 comments · Opened Oct 14, 2026

Maintainers usually reply within 1 day
"Bug in a `do` elaborator" in code combining conditionals and for loops
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 25/100

leanprover/lean4#15685 · Opened Oct 14, 2026

Maintainers usually reply within 1 day
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`
Open
- Is something wrong?
bug

Difficulty 2/5 1-3 hours Newbie friendliness 66/100

leanprover/lean4#15683 · Opened Oct 14, 2026

Maintainers usually reply within 1 day
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)
Open
- Is something wrong?
bug

Difficulty 2/5 1-3 hours Newbie friendliness 70/100

leanprover/lean4#15681 · Opened Oct 14, 2026

Maintainers usually reply within 1 day
`isExclusiveUnsafe` crashes (SIGSEGV) on scalar arguments such as a small `Nat`
Open
- Is something wrong?
bug

Difficulty 2/5 1-3 hours Newbie friendliness 76/100

leanprover/lean4#15677 · Opened Oct 14, 2026

Maintainers usually reply within 1 day
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process group
Open
- Is something wrong?
bug

Difficulty 2/5 1-3 hours Newbie friendliness 72/100

leanprover/lean4#15674 · Opened Oct 14, 2026

Maintainers usually reply within 1 day
letToHave unifies types ignoring transparency seetings
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 30/100

leanprover/lean4#15661 · Opened Oct 13, 2026

Maintainers usually reply within 1 day
`lean --incr-save` never terminates on a file that elaborates in 3 s (`Finsupp.mk ... (fun x => by aesop)`, Mathlib)
Open
- Is something wrong?
Difficulty 5/5 Over a week Newbie friendliness 8/100

leanprover/lean4#15660 · 1 comment · Opened Oct 13, 2026

Maintainers usually reply within 1 day
Diagnostics reused by `--incr-load` carry the saving file's path instead of the current file's path
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/lean4#15658 · 1 comment · Opened Oct 13, 2026

Maintainers usually reply within 1 day
`--incr-save` on top of an `--incr-header-save` snapshot yields a snapshot that fails to load (`invalid 'import' command`) once the file has >= 3 commands
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 30/100

leanprover/lean4#15657 · 1 comment · Opened Oct 13, 2026

Maintainers usually reply within 1 day
`#print axioms` disagrees with the kept theorem body after a duplicate theorem import
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 38/100

leanprover/lean4#15652 · Opened Oct 13, 2026

Maintainers usually reply within 1 day
Windows: copy-on-write .olean mapping (FILE_MAP_COPY) charges the full size of all imported module files to commit (regression since v4.31.0-rc1)
Open
- Is something wrong?
Difficulty 4/5 3-5 days Newbie friendliness 45/100

leanprover/lean4#15644 · Opened Oct 13, 2026

Maintainers usually reply within 1 day
`leanchecker --from-export` rejects string and quotient rfl proof accepted by `Lean`
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 48/100

leanprover/lean4#15643 · 1 comment · Opened Oct 13, 2026

Maintainers usually reply within 1 day
perf: GPT-6.1 Sol says compiler optimization speeds up SHA-256 by 2.36×
Open
- Is something wrong?
Difficulty 5/5 Over a week Newbie friendliness 35/100

leanprover/lean4#15641 · 1 comment · Opened Oct 12, 2026

Maintainers usually reply within 1 day
`grind`: stack overflow on a `match` given the cyclic hypothesis `as = a :: as`
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 45/100

leanprover/lean4#15640 · Opened Oct 12, 2026

Maintainers usually reply within 1 day
Template metadata visible to administrators
Open
- Is something wrong?
enhancement

Difficulty 4/5 3-5 days Newbie friendliness 48/100

leanprover/lean-workbench#182 · Opened Oct 12, 2026

Maintainers usually reply within 1 day
Consider replacing landing page with user profile
Open
- Is something wrong?
Difficulty 2/5 1-3 hours Newbie friendliness 54/100

leanprover/lean-workbench#181 · 1 comment · Opened Oct 12, 2026

Maintainers usually reply within 1 day
cbv trips an internal assertion under -Dsym.debug=true
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 35/100

leanprover/lean4#15633 · Opened Oct 12, 2026

Maintainers usually reply within 1 day
Kernel error: in a mutual block, a sibling’s universe parameter leaks into bar.induct
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 43/100

leanprover/lean4#15632 · Opened Oct 12, 2026

Maintainers usually reply within 1 day
`cbv`: kernel error with a dependent `have` inside an applied lambda
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 48/100

leanprover/lean4#15627 · Opened Oct 12, 2026

Maintainers usually reply within 1 day
Lake: `moreServerOptions` not passed to the server for files inside a library
Open
- Is something wrong?
Difficulty 2/5 1-3 hours Newbie friendliness 82/100

leanprover/lean4#15626 · Opened Oct 12, 2026

Maintainers usually reply within 1 day
`cbv` computes `List.maxOn?` as the minimum
Open
- Is something wrong?
bug

Difficulty 4/5 3-5 days Newbie friendliness 54/100

leanprover/lean4#15625 · Opened Oct 12, 2026

Maintainers usually reply within 1 day

Showing the newest 100

This page lists what was indexed most recently. Advanced filter has the whole inventory, narrowed by language, difficulty and how long a task takes.

Open advanced filter

leanprover

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Is something wrong?

Showing the newest 100

Get new issues in your inbox