Skip to content

Pull requests: leanprover/lean4

New pull request New
449 Open 9,186 Closed
449 Open 9,186 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

refactor: remove dead matcher code from Cbv/Main.lean changelog-tactics User facing tactics
#12568 opened Feb 18, 2026 by wkrozowski Loading…
refactor: rename instance_reducible to implicit_reducible changelog-language Language features and metaprograms
#12567 opened Feb 18, 2026 by leodemoura Loading…
chore: isolate String.length
#12566 opened Feb 18, 2026 by TwoFX • Draft
2
perf: faster Name.quickCmp
#12565 opened Feb 18, 2026 by hargoniX • Draft
8
fix: detect stuck mvars through auxiliary parent projections 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
#12564 opened Feb 18, 2026 by leodemoura Loading…
2
fix: make the omit, unusedSectionVars and loopingSimpArgs linter respect linter.all
#12563 opened Feb 18, 2026 by grunweg Loading…
fix: catch exceptions in cbv rewrite simprocs to handle projections changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12562 opened Feb 18, 2026 by wkrozowski Loading…
1
2
fix: make option linter.unusedSimpArgs respect linter.all builds-manual CI has verified that the Lean Language Reference 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
#12560 opened Feb 18, 2026 by fiforeach • Draft
1
6
experiment alt inc/dec reordering toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12557 opened Feb 18, 2026 by hargoniX • Draft
4
experiment: reuse ite/dite Decidable instance in cbv toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12552 opened Feb 18, 2026 by wkrozowski • Draft
7
refactor: port RC insertion from IR to LCNF toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12548 opened Feb 18, 2026 by hargoniX • Draft
14
chore: simplify a proof in mvcgen test cases and remove duplicate toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12547 opened Feb 18, 2026 by sgraf812 Loading…
2
feat: add lake profile command changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12545 opened Feb 18, 2026 by kim-em • Draft
2
fix: remove transparency bumps from assignOutParams and checkTypesAndAssign awaiting-mathlib We should not merge this until we have a successful Mathlib build 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
#12544 opened Feb 18, 2026 by kim-em • Draft
2
fix(lake): use response files on all platforms to avoid ARG_MAX toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12540 opened Feb 18, 2026 by kim-em Loading…
3
feat: unify name demangling with single Lean implementation changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12539 opened Feb 18, 2026 by kim-em Loading…
10
feat: enable backward.whnf.reducibleClassField 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
#12538 opened Feb 18, 2026 by leodemoura Loading…
2
feat: add pattern-based simproc extension for cbv changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12534 opened Feb 17, 2026 by wkrozowski • Draft
2 tasks done
2
fix: handle stuck sub-args in discrimination tree during TC synthesis toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12528 opened Feb 17, 2026 by nomeata • Draft
3 tasks done
1
2
chore: fix profiler shebang and add profiling skill changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12519 opened Feb 17, 2026 by kim-em Loading…
2
fix: add depth guard to map_map grind_pattern awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-library Library 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
#12515 opened Feb 17, 2026 by kim-em Loading…
3
feat: more reliable universe level inference in inductive/structure commands breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. 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
#12514 opened Feb 17, 2026 by kmill Loading…
5
feat: lake: Shallow git cloning toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12513 opened Feb 16, 2026 by SnO2WMaN • Draft
1
2
test: fill in sorries of grind_qsort.lean test file toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12510 opened Feb 16, 2026 by Seppel3210 Loading…
2
experiment: bv_decide_cbv_decide
#12509 opened Feb 16, 2026 by hargoniX • Draft
1
ProTip! What’s not been updated in a month: updated:<2026-01-18.