Skip to content

Pull requests: leanprover/lean4

New pull request New
350 Open 8,574 Closed
350 Open 8,574 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

feat: add lean-bisect script for bisecting toolchain regressions changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11727 opened Dec 18, 2025 by kim-em Loading…
1 task
3
chore: improve unexpected token messages toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11725 opened Dec 18, 2025 by alok Loading…
3
fix: Signal.Handler segmentation fault with Selector changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11724 opened Dec 18, 2025 by algebraic-dev Loading…
@algebraic-dev
2
feat: add Std.Future to enable IO.Promise-like behavior in Selectable contexts changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11723 opened Dec 17, 2025 by algebraic-dev Loading…
@algebraic-dev
2
perf: match equations: use diteInduction to split breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. 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
#11720 opened Dec 17, 2025 by nomeata • Draft
8
perf: match compilation: pick out overlap assumption directly 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 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
#11711 opened Dec 17, 2025 by nomeata • Draft
5
feat: a grind configuration for use in match equation compilation changelog-language Language features and metaprograms
#11703 opened Dec 16, 2025 by nomeata • Draft
refactor: move error explanation text to the manual 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
#11688 opened Dec 15, 2025 by robsimmons • Draft
2
fix: add missing pp-spaces in grind_pattern toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11686 opened Dec 15, 2025 by adomani • Draft
3
feat: lake: multi-version workspaces breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#11662 opened Dec 14, 2025 by tydeu • Draft
4
chore: add missing .run and .mks in monad transformers
#11647 opened Dec 13, 2025 by eric-wieser • Draft
chore: add header pad on Darwin for patching
#11623 opened Dec 11, 2025 by lenianiva Loading…
2
refactor: grind AIG proofs into dust toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11614 opened Dec 11, 2025 by hargoniX • Draft
2
feat: add grind +simp mode awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-tactics User facing tactics
#11601 opened Dec 11, 2025 by kim-em Loading…
feat: suggestions for some size/count/length confusions changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11588 opened Dec 10, 2025 by robsimmons • Draft
3
feat: grind_pattern mod_eq_of_lt awaiting-review Waiting for someone to review the PR 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-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
#11584 opened Dec 10, 2025 by pirapira Loading…
10
doc: adds missing docstrings related to iterators and ranges changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11563 opened Dec 9, 2025 by david-christiansen Loading…
2
fix: goto-definition for binrel% operators toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11558 opened Dec 9, 2025 by alok • Draft
2
chore: update projection/field access wording toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11533 opened Dec 6, 2025 by robsimmons • Draft
2
feat: use approximate universe inverse when sorry in inductive type toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11524 opened Dec 5, 2025 by kmill • Draft
3
fix: more robust match equation generation 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 force-mathlib-ci 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
#11512 opened Dec 4, 2025 by nomeata • Draft
1
23
feat: termBeforeBy builtin parser 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
#11495 opened Dec 3, 2025 by JovanGerb Loading…
9
feat: add chunking support to par and par' in Lean.Elab.Parallel builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11467 opened Dec 2, 2025 by kim-em • Draft
2
chore: CI: bump actions/checkout from 5 to 6 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11459 opened Dec 1, 2025 by dependabot bot Loading…
2
chore: CI: bump softprops/action-gh-release from 2.4.1 to 2.5.0 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11458 opened Dec 1, 2025 by dependabot bot Loading…
2
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.