leanprover-community/batteries

View on GitHub

The "batteries included" extended library for the Lean programming language and theorem prover

Stars: 419
Forks: 163
Open beginner issues: 0
Indexed issues: 27
Avg merge: 2d 5h
Merged PRs (30d): 14

Dominant language: Lean
License: Apache-2.0
Last GitHub push: Sep 16, 2026
Latest indexed: Sep 18, 2026
Contributing guide: No contributing guide
Code of conduct: No code of conduct
Beginner labels: help wanted

Beginner friendly Everything

Open All

27 open issues indexed

`runLinter` should use lake to find and manage build artifacts Open

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

leanprover-community/batteries#1638 · Opened Jan 27, 2026
RFC: Consider adding Alternative.{many,many1} Open

enhancement

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

leanprover-community/batteries#1577 · 2 comments · Opened Dec 27, 2025
Document what should live here, vs in mathlib Open

documentation question

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

leanprover-community/batteries#1576 · 1 comment · Opened Dec 27, 2025
Simple program causes Lean panic with `Batteries.CodeAction.Match` import Open

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

leanprover-community/batteries#1502 · 6 comments · Opened Nov 8, 2025
Develop the `List.sum`, `List.prod` and related APIs Open

enhancement help wanted

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

leanprover-community/batteries#1465 · 1 comment · Opened Oct 16, 2025
Verify Binary Heap Open

enhancement help wanted

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

leanprover-community/batteries#1442 · 5 comments · Opened Oct 2, 2025
Mathlib CI cache not uploading Open

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

leanprover-community/batteries#1425 · 1 comment · 2 reactions · Opened Sep 22, 2025
batteries CI should run shake Open

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

leanprover-community/batteries#1356 · Opened Jul 31, 2025
`trans` does not work on implicit arguments Open

Difficulty 3/5 1-2 days Newbie friendliness 35/100

leanprover-community/batteries#1222 · 1 comment · Opened May 3, 2025
Run traced_repo = trace(repo) meet the error like KeyError: 'batteries' Open

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

leanprover-community/batteries#1160 · Opened Mar 12, 2025
alias ignores noncomputable section Open

Difficulty 3/5 1-2 days Newbie friendliness 68/100

leanprover-community/batteries#1097 · 1 comment · 2 reactions · Opened Jan 21, 2025
alias does not open namespaces Open

Difficulty 3/5 1-2 days Newbie friendliness 48/100

leanprover-community/batteries#810 · 3 comments · Opened May 25, 2024
`#where` doesn't print `open scoped` Open

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

leanprover-community/batteries#778 · Opened May 2, 2024
Add docker / gitpod integrations Open

Difficulty 3/5 1-2 days Newbie friendliness 38/100

leanprover-community/batteries#565 · 4 comments · Opened Jan 26, 2024
False positive from the unusedHavesSuffices linter Open

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

leanprover-community/batteries#428 · 5 comments · Opened Dec 8, 2023
Codify style guide Open

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

leanprover-community/batteries#336 · Opened Oct 30, 2023
Codify naming conventions Open

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

leanprover-community/batteries#335 · 4 reactions · Opened Oct 30, 2023
Code action for induction ... using ... Open

Difficulty 3/5 1-2 days Newbie friendliness 35/100

leanprover-community/batteries#311 · 1 comment · Opened Oct 21, 2023
`simpNF` gives false positives when the LHS simplifies by a lower priority lemma Open

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

leanprover-community/batteries#207 · Opened Aug 6, 2023
incorrect output from `linter.unnecessarySimpa` Open

Difficulty 3/5 1-2 days Newbie friendliness 45/100

leanprover-community/batteries#180 · 1 reaction · Opened Jul 7, 2023
rcases doesn't seem to support ?_ placeholders Open

Difficulty 3/5 1-2 days Newbie friendliness 42/100

leanprover-community/batteries#116 · 3 comments · 3 reactions · Opened Apr 16, 2023
`@[norm_cast move]` is broken Open

Difficulty 3/5 1-2 days Newbie friendliness 48/100

leanprover-community/batteries#79 · Opened Jan 8, 2023
`simpNF` linter rejecting working simp lemma Open

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

leanprover-community/batteries#71 · 3 comments · Opened Dec 21, 2022
rcases can't use `rfl` on `0 = a` in some circumstances. Open

Difficulty 3/5 1-2 days Newbie friendliness 45/100

leanprover-community/batteries#62 · 6 comments · Opened Dec 8, 2022
`RBMap` etc. should take typeclasses, not explicit comparators Open

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

leanprover-community/batteries#51 · Opened Dec 3, 2022
Cover `mathlib` theorems for `RBMap` Open

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

leanprover-community/batteries#27 · Opened Nov 17, 2022
copyFile Open

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

leanprover-community/batteries#2 · Opened Sep 1, 2022

leanprover-community/batteries

Get new issues in your inbox