Skip to content

Pull requests: leanprover/lean4

New pull request New
390 Open 8,765 Closed
390 Open 8,765 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 two useful lemmas about Int.ediv 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
#12019 opened Jan 15, 2026 by datokrat • Draft
2
feat: various small list/array/vector API improvements breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#12017 opened Jan 15, 2026 by datokrat • Draft
4
perf: separate meta and non-meta initializers
#12016 opened Jan 15, 2026 by Kha • Draft
perf: don't used Inhabited for Array.get! toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12014 opened Jan 15, 2026 by hargoniX • Draft
8
chore: (debug) add tracing to attempt to catch hang 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
#12013 opened Jan 15, 2026 by thorimur • Draft
2
fix: pretty-printing of class abbrev syntax toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12007 opened Jan 14, 2026 by grunweg • Draft
6
perf: make repeat an elaborator
#12002 opened Jan 14, 2026 by Kha • Draft
2
perf: Options.hasTrace 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
#12001 opened Jan 14, 2026 by Kha Loading…
9
feat: lemmas about sums of lists/arrays/vectors breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#11994 opened Jan 13, 2026 by datokrat • Draft
4
chore: remove unused variable in FileMap.ofString toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11986 opened Jan 13, 2026 by ericluap Loading…
2
perf: better derived Hashable for single field structures changelog-library Library
#11984 opened Jan 12, 2026 by hargoniX Loading…
1
2
chore: try printing stack trace on pkg/ test timeout release-ci Enable all CI checks for a PR, like is done for releases
#11980 opened Jan 12, 2026 by Kha • Draft
feat: suggest Int*.toNatClamp for Int*.toNat 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
#11979 opened Jan 12, 2026 by datokrat Loading…
2
feat: more ergonomic error explanation creation changelog-no Do not include this PR in the release changelog
#11975 opened Jan 12, 2026 by robsimmons Loading…
perf: bundle Init into a single big .olean file 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 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
#11965 opened Jan 10, 2026 by Kha • Draft
3 tasks
12
feat: another grind_pattern for getElem?_pos awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-language Language features and metaprograms
#11963 opened Jan 10, 2026 by kim-em • Draft
1
perf: replay tactics when only trailing whitespace is changed 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-server Language server, widgets, and IDE extensions 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
#11958 opened Jan 9, 2026 by Kha • Draft
4
feat: parallel-prefix-sum circuit toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11956 opened Jan 9, 2026 by luisacicolini • Draft
2
chore: lake: fix tests on non-Linux platforms 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 mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11955 opened Jan 9, 2026 by tydeu • Draft
2
chore: inline trace nodes 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
#11954 opened Jan 9, 2026 by eric-wieser Loading…
8
feat: add BitVec.signExtend_extractLsb_setWidth theorem 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
#11943 opened Jan 8, 2026 by osmanyasar05 Loading…
13
feat: projected minima and maxima 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
#11938 opened Jan 8, 2026 by datokrat • Draft
23
feat: min(?)/max(?) for Array 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
#11936 opened Jan 8, 2026 by datokrat Loading…
2
refactor: don't extend Applicative in Alternative 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 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
#11925 opened Jan 7, 2026 by JovanGerb Loading…
3
feat: add typeclass instances for common types awaiting-author Waiting for PR author to address issues toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11924 opened Jan 7, 2026 by alok • Draft
2 tasks done
4
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.