Issues

• decide +kernel hides kernel memory-limit errors when elaborator reduction gets stuck

  leanprover/lean4#16262 · Filter by author BorisTheBrave opened on Nov 4, 2026

• simp [h] cannot use h : ¬ v = 0 on BitVec, because the goal's 0 becomes 0#w before h is tried

  leanprover/lean4#16260 · Filter by author benaadams opened on Nov 4, 2026

• Equation lemmas fail to generate for match id a, a with ...: the hypothesis id 0 = n + 1 is dropped from the statement

  leanprover/lean4#16259 · Filter by author alpaylan opened on Nov 4, 2026

• Std.Time: Duration.toMilliseconds rounds negative durations down (-1ns gives -1ms), unlike the other unit conversions

  leanprover/lean4#16257 · Filter by author alpaylan opened on Nov 4, 2026

• Std.Time: pattern B formats 22:00 as "10:00 at night" but parses it back as 10:00

  leanprover/lean4#16248 · Filter by author alpaylan opened on Nov 4, 2026

• Std.Time: aaaa formats the AM/PM marker as "PM" but parses only "post meridiem", so it cannot read back its own output

  leanprover/lean4#16247 · Filter by author alpaylan opened on Nov 4, 2026

• grind_pattern after attribute [-grind] revives the erased pattern

  leanprover/lean4#16244 · Filter by author sgraf812 opened on Nov 4, 2026

• Kernel rejects structure J : Type (u+1) where x : Sort (imax (u+1) u) as "too big", though the elaborator accepts it

  leanprover/lean4#16242 · Filter by author alpaylan opened on Nov 4, 2026
  1

• WorkspaceEdits fail when targeting a URI without a version

  bug
  leanprover/lean4#16236 · Filter by author thorimur opened on Nov 3, 2026

• Kernel refuses 2 ^ 16777217 as over the numeral size limit, though the result is 2 MB of the 128 MB budget

  leanprover/lean4#16230 · Filter by author alpaylan opened on Nov 3, 2026

• lia/grind: kernel rejects the proof of x % 3 ≤ 2 * x % 3 → 4 * x % 3 ≤ 2 * x % 3 (eq_of_dvd_ediv type mismatch)

  grind
  leanprover/lean4#16228 · Filter by author alpaylan opened on Nov 3, 2026

• List.take_add as @[grind =] matches its own result and exhausts the instance budget

  leanprover/lean4#16223 · Filter by author sgraf812 opened on Nov 3, 2026

• decreasing_tactic fails for structure projections

  bug
  leanprover/lean4#16209 · Filter by author TwoFX opened on Nov 3, 2026
  2

• IO.FS.withTempDir segfaults when TMPDIR points to a missing directory

  leanprover/lean4#16202 · Filter by author douglaz opened on Nov 3, 2026

• With compiler.postponeCompile, leanir fails with `Unknown constant _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map on any use of Array.map`

  leanprover/lean4#16201 · Filter by author alpaylan opened on Nov 3, 2026

• PANIC "getOptions called inside a computation recording its dependencies" when logAt warns during instance synthesis (decide on BitVec.twoPow 276)

  leanprover/lean4#16197 · Filter by author alpaylan opened on Nov 2, 2026

• Confusing error when trying to derive instance for compound type

  bug
  leanprover/lean4#16189 · Filter by author FeldrinH opened on Nov 2, 2026

• Deprecations generate multiple try this: suggestions for rewrites at multiple locations

  bug
  leanprover/lean4#16184 · Filter by author grunweg opened on Nov 2, 2026

• RFC: initialise top-level constants lazily, as closed terms already are

  leanprover/lean4#16179 · Filter by author matthiasgoergens opened on Nov 2, 2026

• IO.sleep never returns while its thread is interrupted by frequent signals

  leanprover/lean4#16171 · Filter by author matthiasgoergens opened on Nov 2, 2026

• Kernel exhausts memory checking (x + BitVec.ofNat 64 C).toNat = … by rfl (the @[defeq] lemma BitVec.toNat_add), cost growing with the literal C

  leanprover/lean4#16170 · Filter by author alpaylan opened on Nov 2, 2026
  1

• Expose the logical range-loop body for kernel reduction in modules

  leanprover/lean4#16169 · Filter by author kim-em opened on Nov 2, 2026

• With compiler.extract_closed false, borrow inference treats string and big Nat literals as borrowed: use after free and wrong results

  code-generator
  leanprover/lean4#16160 · Filter by author alpaylan opened on Nov 1, 2026

• [4.34] simp rewriting of decide p = true (via core decide_eq_true_eq) changes term shape, breaking nested projections

  leanprover/lean4#16154 · Filter by author JaneConan opened on Nov 1, 2026
  1

• RFC: Improve Semantic Highlighting

  RFC
  leanprover/lean4#16150 · Filter by author RIvance opened on Nov 1, 2026
  1