Skip to content

Pull requests: leanprover/lean4

New pull request New
448 Open 9,247 Closed
448 Open 9,247 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 pull_request_target for label-triggered workflows changelog-other
#12638 opened Feb 22, 2026 by kim-em Loading…
feat: limit the use of Classical.choice toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12637 opened Feb 22, 2026 by riccardobrasca • Draft
2
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
3
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
fix: mark failed compilations as noncomputable backport releases/v4.29.0 breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-compiler Compiler, runtime, and FFI 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
#12625 opened Feb 20, 2026 by Kha Loading…
7
chore: CLAUDE.md: restrict build parallelism toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12624 opened Feb 20, 2026 by Kha Loading…
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
doc: add module and function docstrings for cbv tactic changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12616 opened Feb 20, 2026 by wkrozowski Loading…
2
feat: clean up binder annotations inside of let rec definitions 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
#12608 opened Feb 20, 2026 by kmill Loading…
1
2
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: pp.mdata 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
#12606 opened Feb 20, 2026 by kmill Loading…
1
3
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
#12590 opened Feb 19, 2026 by Garmelon • Draft
6
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
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…
13
fix: make the omit, unusedSectionVars and loopingSimpArgs linter respect linter.all changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12563 opened Feb 18, 2026 by grunweg Loading…
9
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 Loading…
1
19
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
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.