Skip to content

Pull requests: leanprover/lean4

New pull request New
450 Open 9,339 Closed
450 Open 9,339 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

fix: use _fvar._ instead of _ for anonymous fvars backport releases/v4.29.0 changelog-pp Pretty printing
#12745 opened Mar 1, 2026 by kim-em • Queued
[Backport releases/v4.29.0] feat: add pp.fvars.anonymous option
#12744 opened Mar 1, 2026 by github-actions bot Loading…
[Backport releases/v4.29.0] fix: mark levelZero, levelOne, and Level.ofNat as implicit_reducible
#12743 opened Mar 1, 2026 by github-actions bot Loading…
feat: add Scan iterator combinator toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12742 opened Mar 1, 2026 by cmlsharp Loading…
1
2
fix: make sure AbstracNestedProofs.visit doesn't fail due to transparency issues builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12740 opened Feb 28, 2026 by arthur-adjedj Loading…
6
fix: notify LSP client when worker process crashes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12736 opened Feb 28, 2026 by wvhulle Loading…
2
fix: guard LSP refresh requests behind capability check toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12735 opened Feb 28, 2026 by wvhulle Loading…
1
2
fix: kernel: move level parameter count and thm-is-prop checks for robustness changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12734 opened Feb 28, 2026 by Copilot AI Loading…
1
@nomeata
14
feat: XID support in Lean identifiers toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12726 opened Feb 27, 2026 by hargoniX • Draft
6
chore: deprecate levelZero and levelOne toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12720 opened Feb 27, 2026 by kim-em Loading…
2
feat: generalize below and brecOn on subsingletons builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12718 opened Feb 26, 2026 by arthur-adjedj Loading…
1
19
feat: standalone List.extract lemmas, don't normalize extract into drop/take changelog-library Library
#12703 opened Feb 26, 2026 by datokrat • Draft
fix: validate stage0 version matches release version changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12700 opened Feb 26, 2026 by kim-em Loading…
1
5
feat: add structured TraceResult to TraceData toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12698 opened Feb 26, 2026 by kim-em • Draft
4
feat: add cslib package template toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12679 opened Feb 24, 2026 by Shreyas4991 • Draft
1
2
perf: simplify cbv ite/dite simprocs by reducing Decidable instance directly changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12677 opened Feb 24, 2026 by wkrozowski Loading…
4
feat: leading whitespace on first token builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12662 opened Feb 23, 2026 by mhuisi Loading…
6
feat: add ground evaluation for And/Or in Sym.Simp changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12660 opened Feb 23, 2026 by wkrozowski Loading…
4
fix: detect native c++ stdlib instead of hard-coding for darwin toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12659 opened Feb 23, 2026 by jacobly0 • Draft
1
2
perf: persist grind preprocessing caches across calls changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12657 opened Feb 23, 2026 by sgraf812 • Draft
2 tasks done
4
chore: turn on new do elaborator in Core toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN unlock-upstream-stdlib-flags
#12656 opened Feb 23, 2026 by sgraf812 Loading…
28
experiment: fix various eta issues breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12636 opened Feb 21, 2026 by arthur-adjedj • Draft
1
19
feat: lake: download artifacts on demand builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12634 opened Feb 21, 2026 by tydeu • Draft
5
feat: add .claude/settings.json to lake init templates changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12632 opened Feb 21, 2026 by kim-em Loading…
2
experiment: type improvements toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12631 opened Feb 20, 2026 by hargoniX • Draft
4
ProTip! no:milestone will show everything without a milestone.