Search results

linter.unusedSectionVars: does not detect variable uses in where clauses

Status: Open.

#11917 In leanprover/lean4;

· kim-em opened on Jan 6, 2026

panic in grind

Status: Open.

#11910 In leanprover/lean4;

· kim-em opened on Jan 6, 2026

grind: cannot teach grind that (¬(x = none)) -> (∃ y, x = some y)

bugSomething isn't workingSomething isn't working

Status: Open.

#11897 In leanprover/lean4;

· safinaskar opened on Jan 5, 2026

"This pattern contains metavariables" when using structure constructor and omitting a proof parameter

bugSomething isn't workingSomething isn't working

Status: Open.

#11885 In leanprover/lean4;

· kmill opened on Jan 3, 2026

<code>conv in</code> can unexpectedly fail with <code>unknown metavariable</code> error

bugSomething isn't workingSomething isn't working

Status: Open.

#11877 In leanprover/lean4;

· vlad902 opened on Jan 2, 2026

grind/grobner doesn't finish a proof for a medium-sized problem within reasonable limit

low priority

performanceA performance problem related issue or PRA performance problem related issue or PR

Status: Open.

#11861 In leanprover/lean4;

· wwylele opened on Jan 1, 2026

Inductive type declaration UX bug involving a <code>where</code> typo

bugSomething isn't workingSomething isn't working

Status: Open.

#11853 In leanprover/lean4;

· Chris-F5 opened on Dec 31, 2025

<code>sizeOf</code> generation failure on higher-order nested types

bugSomething isn't workingSomething isn't working

Status: Open.

#11828 In leanprover/lean4;

· arthur-adjedj opened on Dec 29, 2025

Compiler crashes on modules that import both a precompiled library and <code>Lake.CLI</code>

bugSomething isn't workingSomething isn't working

Status: Open.

#11827 In leanprover/lean4;

· zqy1018 opened on Dec 29, 2025

"The recommended spelling of ¬ in identifiers is not" is wrong

bugSomething isn't workingSomething isn't working

Status: Open.

#11826 In leanprover/lean4;

· safinaskar opened on Dec 29, 2025

<code>declare_syntax_cat</code> in private section causes "unknown constant" on import

bugSomething isn't workingSomething isn't working

Status: Open.

#11823 In leanprover/lean4;

· datokrat opened on Dec 29, 2025

RFC: improving performance of <code>deriving Hashable</code> on single-field structures

RFCRequest for commentsRequest for comments

Status: Open.

#11818 In leanprover/lean4;

· math-fehr opened on Dec 28, 2025