Skip to content

Pull requests: leanprover/lean4

New pull request New
397 Open 8,782 Closed
397 Open 8,782 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: make first token detection work in modules changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12047 opened Jan 19, 2026 by david-christiansen Loading…
1
7
fix: set data? field in all unknown identifier code actions changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12046 opened Jan 19, 2026 by mhuisi Loading…
2
chore: lake: disable import all check (for now) 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
#12045 opened Jan 19, 2026 by tydeu • Draft
2
feat: lazy initialization of closed terms
#12044 opened Jan 19, 2026 by hargoniX • Draft
8
feat: generalize basic Inhabited/Nonempty instances from Monad to Applicative toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12041 opened Jan 19, 2026 by fgdorais Loading…
1
2
fix: lake: cache blockers for CI integration 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
#12037 opened Jan 18, 2026 by tydeu • Draft
2
feat: link OpenSSL toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12030 opened Jan 16, 2026 by algebraic-dev • Draft
@algebraic-dev
2
experiment: immediate noncomputable check 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
#12028 opened Jan 16, 2026 by Kha • Draft
2
perf: use static initializers where possible changelog-compiler Compiler, runtime, and FFI
#12023 opened Jan 16, 2026 by hargoniX • Draft
12
perf: link with identical code folding toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12022 opened Jan 16, 2026 by Kha • Draft
6
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 Loading…
2
feat: various small list/array/vector API improvements 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
#12017 opened Jan 15, 2026 by datokrat Loading…
5
perf: separate meta and non-meta initializers
#12016 opened Jan 15, 2026 by Kha • Draft
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
3
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
feat: lemmas about sums of lists/arrays/vectors 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
#11994 opened Jan 13, 2026 by datokrat Loading…
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
ProTip! Filter pull requests by the default branch with base:master.