Issues

• Track examples where ring succeeds but grobner fails

  leanprover/lean4#15480 · Filter by author kim-em opened on Oct 5, 2026

• grind: internal error on symbolic powers in semirings

  leanprover/lean4#15479 · Filter by author kim-em opened on Oct 5, 2026

• RCases.rcasesCore (rcases/obtain/rintro) takes Θ(n⁴) time for a pattern with n names

  bug
  leanprover/lean4#15477 · Filter by author fNBU opened on Oct 4, 2026

• "Go to definition" does nothing in the definition of a child field that use a parent structure's field

  bug
  leanprover/lean4#15472 · Filter by author user202729 opened on Oct 4, 2026
  1

• Std.Http server Date header uses +0000 instead of the GMT form required by RFC 9110

  bug
  leanprover/lean4#15468 · Filter by author carlohamalainen opened on Oct 4, 2026

• assertion violation: recInfo.numMotives = igi.numMotives in nestedTypeFormers

  bug
  leanprover/lean4#15462 · Filter by author Koukyosyumei opened on Oct 3, 2026

• Panic assertion violation: start < stop in cbv on ill-formed constructor arguments

  bug
  leanprover/lean4#15455 · Filter by author Koukyosyumei opened on Oct 3, 2026
  1

• Uncaught lean::exception in Lean.Elab.process causes process abort (SIGABRT)

  bug
  leanprover/lean4#15453 · Filter by author Koukyosyumei opened on Oct 3, 2026

• Panic in FunInd.buildInductionBody when definition has a duplicate match arm

  bug
  leanprover/lean4#15452 · Filter by author Koukyosyumei opened on Oct 3, 2026

• Kernel defeq compares the continuations that bind (.error e) _ discards (and #8309 doubled the cost)

  leanprover/lean4#15447 · Filter by author kim-em opened on Oct 3, 2026
  3

• Std.Http server sends no response when the system has no timezone database

  bug
  leanprover/lean4#15442 · Filter by author carlohamalainen opened on Oct 2, 2026

• Code generator panic: LCNF ExplicitBoxing "unreachable code" + IR check failure

  bug
  leanprover/lean4#15441 · Filter by author Koukyosyumei opened on Oct 2, 2026

• Internal panic generating equation lemma: "unknown metavariable" + kernel rejection

  bug
  leanprover/lean4#15440 · Filter by author Koukyosyumei opened on Oct 2, 2026

• Nat.pow crashes the process with SIGFPE for large results (multi-limb base)

  bug
  leanprover/lean4#15439 · Filter by author Koukyosyumei opened on Oct 2, 2026

• Lake: facet keys in needs can create duplicate build jobs

  leanprover/lean4#15435 · Filter by author rbeauchamp opened on Oct 2, 2026

• Autocomplete gives unwanted items containing symbols in their names

  bug
  leanprover/lean4#15432 · Filter by author Bubbler-4 opened on Oct 2, 2026

• WPMonad.withFrameClosure restricted to m : Type → Type and R : Type

  bug
  leanprover/lean4#15424 · Filter by author szch79 opened on Oct 1, 2026

• Wrong SymM maximal sharing behavior for letE

  bug
  leanprover/lean4#15423 · Filter by author szch79 opened on Oct 1, 2026

• module system: addDecl accepts public declarations whose exported type mentions private constants

  leanprover/lean4#15401 · Filter by author marcelolynch opened on Sep 29, 2026
  1

• module system: by blocks in variable binders inside public section put unexported aux proofs into public signatures

  leanprover/lean4#15393 · Filter by author marcelolynch opened on Sep 28, 2026
  1

• bv_decide no longer reifies a BitVec atom reached through a @[reducible] accessor over a structure field whose width is computed by a def (regression in v4.34.0)

  leanprover/lean4#15368 · Filter by author Calgooon opened on Sep 27, 2026

• Compiler PANIC in ExplicitBoxing when an auto-generated SizeOf instance reaches codegen (regression since 4.28)

  bug
  leanprover/lean4#15346 · Filter by author rvs314 opened on Sep 26, 2026
  1

• getMainModule breaks when accessing files through URIs with #-fragments

  bug
  leanprover/lean4#15342 · Filter by author thorimur opened on Sep 26, 2026

• The test lake/tests/cacheTransfer fails

  leanprover/lean4#15335 · Filter by author yurivict opened on Sep 25, 2026
  1

• Tests don't respect the CTEST_PARALLEL_LEVEL environment variable

  leanprover/lean4#15334 · Filter by author yurivict opened on Sep 25, 2026