Skip to content

Pull requests: leanprover/lean4

New pull request New
451 Open 9,279 Closed
451 Open 9,279 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

chore: tighten a do match elaborator test case to prevent global defaulting
#12675 opened Feb 24, 2026 by sgraf812 Loading…
perf: speedup unexpanded reset-reuse pairs toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12672 opened Feb 24, 2026 by hargoniX • Draft
6
feat: non exponential codegen for reset-reuse changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12665 opened Feb 23, 2026 by hargoniX • Draft
16
feat: leading whitespace on first token breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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…
2
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 • Draft
21
fix: pretty printing constants should use accessibility of names builds-mathlib CI has verified that Mathlib builds against this PR changelog-pp Pretty printing 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
#12654 opened Feb 23, 2026 by kmill Loading…
1
3
chore: relative lean-toolchains builds-mathlib CI has verified that Mathlib builds against this PR 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
#12652 opened Feb 23, 2026 by mhuisi Loading…
2
fix: withNamespace now correctly calls popScopes after running changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12647 opened Feb 23, 2026 by wkrozowski • Queued
1
2
fix: use pull_request_target for label-triggered workflows changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12638 opened Feb 22, 2026 by kim-em Loading…
5
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
9
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
2
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
cleanup: remove unused argument from ExceptCps.runK toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12628 opened Feb 20, 2026 by andres-erbsen • Draft
2
perf: only instantiate mvars in RHS of simp theorem builds-mathlib CI has verified that Mathlib builds against this PR 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
#12618 opened Feb 20, 2026 by JovanGerb Loading…
6
fix: make tactic .. at * save info contexts builds-mathlib CI has verified that Mathlib builds against this PR changelog-tactics User facing tactics 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
#12607 opened Feb 20, 2026 by kmill Loading…
1
2
feat: overriding binder kinds of parameters in inductive constructors 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
#12603 opened Feb 20, 2026 by kmill Loading…
3
[REBASED] feat: strengthen evalConst meta check builds-mathlib CI has verified that Mathlib builds against this PR fast-ci Forces the use of large runners so that e.g. PR releases are created faster 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
#12602 opened Feb 19, 2026 by Kha • Draft
7
feat: add cbv_simproc infrastructure for user-extensible cbv simplification procedures changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12597 opened Feb 19, 2026 by wkrozowski Loading…
2
chore: set up new test/bench suite toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12590 opened Feb 19, 2026 by Garmelon Loading…
12
feat: add mkSimprocPatternFromExpr for creating patterns from expressions with metavariables toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12569 opened Feb 18, 2026 by wkrozowski • Draft
2
chore: isolate String.length changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12566 opened Feb 18, 2026 by TwoFX • Draft
6
ProTip! no:milestone will show everything without a milestone.