Skip to content

Pull requests: leanprover/lean4

New pull request New
389 Open 8,759 Closed
389 Open 8,759 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: (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
feat: allow go-to-projection to look through reducible definitions 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
#12004 opened Jan 14, 2026 by mhuisi Loading…
2
perf: make repeat an elaborator
#12002 opened Jan 14, 2026 by Kha • Draft
2
perf: Options.hasTrace 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 • Draft
6
wip: human-eval-lean upstreaming 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
#11994 opened Jan 13, 2026 by datokrat • Draft
4
feat: add grind annotations for list and array slices 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
#11993 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 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
#11965 opened Jan 10, 2026 by Kha • Draft
3 tasks
10
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
15
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
feat: add lake shake command changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11921 opened Jan 7, 2026 by kim-em • Draft
9
fix: warn when Where is used instead of where in declarations changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11904 opened Jan 5, 2026 by kim-em Loading…
1
5
ProTip! Exclude everything labeled bug with -label:bug.