Search results

Lake compile scheduler can overcommit Lean worker pools on large import graphs, causing macOS SoC watchdog resets

bugSomething isn't workingSomething isn't working

Status: Open.

#13767 In leanprover/lean4;

· chris-hypernym opened on May 18, 2026

invalid anchors when passing a typeclass to grind

bugSomething isn't workingSomething isn't working

Status: Open.

#13764 In leanprover/lean4;

· chenson2018 opened on May 17, 2026

Circular wording in #eval docstring

Status: Open.

#13753 In leanprover/lean4;

· thomasjbetsworth opened on May 16, 2026

mepo: score function over-rewards tiny generic theorems

Status: Open.

#13749 In leanprover/lean4;

· kim-em opened on May 16, 2026

#grind_lint does not recognize grind sets

bugSomething isn't workingSomething isn't working

Status: Open.

#13733 In leanprover/lean4;

· chenson2018 opened on May 14, 2026

grind fails when tagging an unrelated lemma

bugSomething isn't workingSomething isn't working

Status: Open.

#13725 In leanprover/lean4;

· fpvandoorn opened on May 13, 2026

Misleading simp mention in cbv error message

bugSomething isn't workingSomething isn't working

Status: Open.

#13719 In leanprover/lean4;

· juanjomadrigal opened on May 12, 2026

RFC: Add Array.mapA

RFCRequest for commentsRequest for comments

Status: Open.

#13714 In leanprover/lean4;

· srghma opened on May 12, 2026

Proposal: Four-Tier Library Architecture & Version Governance

RFCRequest for commentsRequest for comments

Status: Open.

#13713 In leanprover/lean4;

· ZhangJun1972 opened on May 12, 2026

exact? and grind block on prior async theorem bodies

bugSomething isn't workingSomething isn't working

P-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the time

Status: Open.

#13705 In leanprover/lean4;

· nomeata opened on May 11, 2026

mconstructor / mleft is incompatible with mhave's state

bugSomething isn't workingSomething isn't working

P-mediumWe may work on this issue if we find the timeWe may work on this issue if we find the time

Status: Open.

#13691 In leanprover/lean4;

· mirefek opened on May 8, 2026

IR eta-expansion through trivial structure

bugSomething isn't workingSomething isn't working

code-generatorThis issue is with the code generatorThis issue is with the code generator

Status: Open.

#13685 In leanprover/lean4;

· sgraf812 opened on May 7, 2026