Issues

• segfault @[try_suggestion] accepts a suggester whose type gained section variables in a mutual block

  bug
  leanprover/lean4#15744 · Filter by author YuanchengJiang opened on Oct 16, 2026

• mkValueTypeClosure type-checks closed terms when the local context has a let

  bug
  leanprover/lean4#15742 · Filter by author Kha opened on Oct 16, 2026

• building 4.35 now requires git checkout for lean4lean

  leanprover/lean4#15741 · Filter by author juhp opened on Oct 16, 2026
  4

• Equation lemmas fail to generate for structural recursion through match on the decreasing argument and a value bound by a monadic bind

  leanprover/lean4#15735 · Filter by author nomeata opened on Oct 16, 2026

• vcgen: a spec whose argument contains a pattern-matching lambda does not apply to the same program elaborated in another module

  leanprover/lean4#15734 · Filter by author nomeata opened on Oct 16, 2026

• vcgen: a callee spec's argument fixed only by its precondition stays a metavariable

  leanprover/lean4#15733 · Filter by author nomeata opened on Oct 16, 2026

• vcgen: spec not applicable when a program argument is a projection (mk e).env that reduces to the spec's argument

  leanprover/lean4#15732 · Filter by author nomeata opened on Oct 16, 2026

• vcgen: no spec found for a call through a structure projection ops.op x with ops a concrete instance

  leanprover/lean4#15731 · Filter by author nomeata opened on Oct 16, 2026

• vcgen: "Failed to apply split rule" for an over-applied ite, (if c then f else g) x

  leanprover/lean4#15730 · Filter by author nomeata opened on Oct 16, 2026

• vcgen: an equation in the spec list whose left-hand side is an ite program is not used; the ite is split first

  leanprover/lean4#15729 · Filter by author nomeata opened on Oct 16, 2026

• vcgen: no f.eq_def fallback for a recursive function whose equation lemmas are conditional ("No spec found")

  leanprover/lean4#15728 · Filter by author nomeata opened on Oct 16, 2026

• grind: kernel rejects a proof that puts a Vector Nat n atom into an RArray Nat

  bug
  leanprover/lean4#15726 · Filter by author Leo0506 opened on Oct 16, 2026

• @[always_inline, inline] is a leftover from the old code generator

  leanprover/lean4#15722 · Filter by author user470750 opened on Oct 15, 2026

• grind: kernel error with equations between constant functions

  bug
  leanprover/lean4#15721 · Filter by author Leo0506 opened on Oct 15, 2026

• Unused untyped variable declaration breaks deriving DecidableEq

  bug
  leanprover/lean4#15720 · Filter by author procoderxx opened on Oct 15, 2026

• Definition of ST.Ref allows for unsafe cast between any two Types in BaseIO

  bug
  leanprover/lean4#15717 · Filter by author Rob23oba opened on Oct 15, 2026
  2

• vcgen frames fails on types with abbreviation

  bug
  leanprover/lean4#15713 · Filter by author szch79 opened on Oct 15, 2026

• Kernel: is_def_eq remains order-dependent via is_def_eq_binding right-bias and m_eager_reduce cache pollution

  leanprover/lean4#15706 · Filter by author gersh opened on Oct 15, 2026

• Kernel: check_recursors uses tcheck.infer(reduct) (infer_only = true), leaving generated induction hypotheses v untypechecked

  leanprover/lean4#15705 · Filter by author gersh opened on Oct 15, 2026

• Kernel soundness: unverified consume_type_annotations and parameter domain mismatch in elim_only_at_universe_zero allow large elimination from Prop

  leanprover/lean4#15704 · Filter by author gersh opened on Oct 15, 2026

• grind: kernel error because abstractGroundMismatches? passes the abstracted terms in reverse order

  bug
  leanprover/lean4#15700 · Filter by author Leo0506 opened on Oct 15, 2026

• lia: kernel error in eq_def_struct with a dependent Int field (regression)

  bug
  leanprover/lean4#15699 · Filter by author Leo0506 opened on Oct 15, 2026

• grind: hypothesis treated as a match condition fails depending on hypothesis order (nested constructor pattern)

  bug
  leanprover/lean4#15697 · Filter by author nomeata opened on Oct 14, 2026
  1

• 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

  leanprover/lean4#15694 · Filter by author kevinsullivan opened on Oct 14, 2026

• IO.appPath fails when /proc belongs to another PID namespace

  bug
  leanprover/lean4#15692 · Filter by author treiher opened on Oct 14, 2026