Skip to content

Pull requests: leanprover/lean4

New pull request New
405 Open 8,795 Closed
405 Open 8,795 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

Rc plus tracing
#12078 opened Jan 21, 2026 by marcelolynch • Draft
doc: document rewrite, rw and rwa according to new guidelines
#12074 opened Jan 20, 2026 by Vierkantor Loading…
perf: more tweaks to injEq generation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12073 opened Jan 20, 2026 by nomeata • Draft
12
perf: Nat.testBit builtin no-alloc implementation 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
#12071 opened Jan 20, 2026 by Kha • Draft
4
perf: make Environment.getModuleIdx? constant-time 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
#12068 opened Jan 20, 2026 by Kha • Draft
6
perf: strip unneeded symbols from libleanshared* 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
#12060 opened Jan 20, 2026 by hargoniX Loading…
4
feat: bijection between Char and Fin Char.numCodePoints toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet.
#12058 opened Jan 20, 2026 by TwoFX • Draft
2
(draft) patch rc with race fix toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12054 opened Jan 20, 2026 by marcelolynch Loading…
2
fix: Avoid deadlock by not throttling workers when the task manager is shutting down toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12052 opened Jan 20, 2026 by marcelolynch Loading…
4
fix: potential deadlock on thread pool shutdown toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12050 opened Jan 19, 2026 by Kha • Draft
4
test PR for !bench (don't merge) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12049 opened Jan 19, 2026 by Garmelon • Draft
4
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
5
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
16
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
ProTip! Filter pull requests by the default branch with base:master.