Issues

• runLinter should use lake to find and manage build artifacts

  leanprover-community/batteries#1638 · Filter by author thorimur opened on Jan 27, 2026

• RFC: Consider adding Alternative.{many,many1}

  enhancement
  leanprover-community/batteries#1577 · Filter by author 414owen opened on Dec 27, 2025
  2

• Document what should live here, vs in mathlib

  documentationquestion
  leanprover-community/batteries#1576 · Filter by author 414owen opened on Dec 27, 2025
  1

• Simple program causes Lean panic with Batteries.CodeAction.Match import

  leanprover-community/batteries#1502 · Filter by author mik-jozef opened on Nov 8, 2025
  6

• Develop the List.sum, List.prod and related APIs

  enhancementhelp wanted
  Feature

  leanprover-community/batteries#1465 · Filter by author fgdorais opened on Oct 16, 2025
  1

• Verify Binary Heap

  enhancementhelp wanted
  Feature

  leanprover-community/batteries#1442 · Filter by author fgdorais opened on Oct 2, 2025
  5

• Mathlib CI cache not uploading

  leanprover-community/batteries#1425 · Filter by author wrenna-robson opened on Sep 22, 2025
  1

• batteries CI should run shake

  leanprover-community/batteries#1356 · Filter by author kim-em opened on Jul 31, 2025

• trans does not work on implicit arguments

  leanprover-community/batteries#1222 · Filter by author staroperator opened on May 3, 2025
  1

• Run traced_repo = trace(repo) meet the error like KeyError: 'batteries'

  leanprover-community/batteries#1160 · Filter by author zx1384187 opened on Mar 12, 2025

• alias ignores noncomputable section

  leanprover-community/batteries#1097 · Filter by author YaelDillies opened on Jan 21, 2025
  1

• alias does not open namespaces

  leanprover-community/batteries#810 · Filter by author YaelDillies opened on May 25, 2024
  3

• #where doesn't print open scoped

  leanprover-community/batteries#778 · Filter by author fpvandoorn opened on May 2, 2024

• Add docker / gitpod integrations

  leanprover-community/batteries#565 · Filter by author alexjbest opened on Jan 26, 2024
  4

• False positive from the unusedHavesSuffices linter

  leanprover-community/batteries#428 · Filter by author kim-em opened on Dec 8, 2023
  5

• Codify style guide

  leanprover-community/batteries#336 · Filter by author digama0 opened on Oct 30, 2023

• Codify naming conventions

  leanprover-community/batteries#335 · Filter by author joehendrix opened on Oct 30, 2023

• Code action for induction ... using ...

  leanprover-community/batteries#311 · Filter by author PatrickMassot opened on Oct 21, 2023
  1

• simpNF gives false positives when the LHS simplifies by a lower priority lemma

  leanprover-community/batteries#207 · Filter by author kim-em opened on Aug 6, 2023

• incorrect output from linter.unnecessarySimpa

  leanprover-community/batteries#180 · Filter by author kbuzzard opened on Jul 7, 2023

• rcases doesn't seem to support ?_ placeholders

  leanprover-community/batteries#116 · Filter by author Ruben-VandeVelde opened on Apr 16, 2023
  3

• @[norm_cast move] is broken

  leanprover-community/batteries#79 · Filter by author gebner opened on Jan 8, 2023

• simpNF linter rejecting working simp lemma

  leanprover-community/batteries#71 · Filter by author kbuzzard opened on Dec 21, 2022
  3

• rcases can't use rfl on 0 = a in some circumstances.

  leanprover-community/batteries#62 · Filter by author kim-em opened on Dec 8, 2022
  6

• RBMap etc. should take typeclasses, not explicit comparators

  leanprover-community/batteries#51 · Filter by author Kha opened on Dec 3, 2022