Skip to content

Pull requests: leanprover/lean4

New pull request New
409 Open 8,807 Closed
409 Open 8,807 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: make Verso module docstring API more like that for Markdown changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12093 opened Jan 21, 2026 by david-christiansen Loading…
2
chore: make bench suite more similar to mathlib's toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12091 opened Jan 21, 2026 by Garmelon • Draft
8
fix: Wake up throttled workers on shutdown toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12090 opened Jan 21, 2026 by marcelolynch Loading…
3
refactor: eliminate FileIdent.mod toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12089 opened Jan 21, 2026 by mhuisi Loading…
2
fix: lake: --no-build failure w/ optional release fetch 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
#12086 opened Jan 21, 2026 by tydeu • Draft
2
refactor: remove redundant calls to DocumentMeta.mod toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12085 opened Jan 21, 2026 by mhuisi Loading…
2
perf: experiment: elaborate primitive recursive funcions to .rec
#12084 opened Jan 21, 2026 by nomeata • Draft
2
feat: use static initializers where possible changelog-compiler Compiler, runtime, and FFI release-ci Enable all CI checks for a PR, like is done for releases
#12082 opened Jan 21, 2026 by hargoniX Loading…
2
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: 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: Fin and Char ranges 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-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
#12058 opened Jan 20, 2026 by TwoFX Loading…
7
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…
5
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
12
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: 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
ProTip! Updated in the last three days: updated:>2026-01-18.