Skip to content

Pull requests: leanprover/lean4

New pull request New
485 Open 9,696 Closed
485 Open 9,696 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 letConfig support to do block let/have changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13215 opened Mar 31, 2026 by sgraf812 • Draft
2
experiment: add optional check_system interval monitoring 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
#13212 opened Mar 31, 2026 by nomeata • Draft
1
feat: add unlock_limits command to disable all resource limits 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
#13211 opened Mar 31, 2026 by Kha Loading…
2
test: lazy let-binding unfolding in sym mvcgen changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13210 opened Mar 31, 2026 by sgraf812 • Draft
4
feat: verifiable repeat/while loops changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13209 opened Mar 31, 2026 by sgraf812 • Draft
2
chore: strip binaries only in release builds toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13208 opened Mar 31, 2026 by Garmelon Loading…
2
feat: add try? => tac syntax and fix asTask subtask cancellation 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
#13206 opened Mar 31, 2026 by nomeata • Draft
2
fix: make FirstTokens.seq (.optTokens _) .unknown return .unkown changelog-language Language features and metaprograms
#13205 opened Mar 31, 2026 by Rob23oba Loading…
1
2
fix: avoid heartbeat timeout in symbolFrequencyExt export builds-mathlib CI has verified that Mathlib builds against this PR changelog-tactics User facing tactics 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
#13202 opened Mar 31, 2026 by Kha Loading…
1
2
feat: add List.prod, Array.prod, and Vector.prod changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13200 opened Mar 31, 2026 by kim-em Loading…
2
fix: handle numerals in non-tail positions of cutsat polynomials changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13199 opened Mar 31, 2026 by kim-em Loading…
2
fix: docstring errors toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13198 opened Mar 30, 2026 by dfpetrin Loading…
3
chore: use FetchContent for mimalloc source acquisition toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13196 opened Mar 30, 2026 by nadja-y • Draft
1
2
feat: allow deprecating options changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13195 opened Mar 30, 2026 by wkrozowski Loading…
2
feat: add closure support to the object compactor 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
#13194 opened Mar 30, 2026 by Kha • Draft
4
perf: replace global task_finished_cv with per-task waiter notifications 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
#13191 opened Mar 30, 2026 by Kha • Draft
5
perf: don't optimize dead specializations toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13187 opened Mar 30, 2026 by hargoniX • Draft
4
feat: add saveModuleDataIncr/readModuleDataIncr with dep region sharing builds-mathlib CI has verified that Mathlib builds against this PR changelog-other 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
#13185 opened Mar 30, 2026 by Kha Loading…
10
feat: add pp.memoize option for compact pretty-printing with shared subexpressions changelog-pp Pretty printing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13183 opened Mar 30, 2026 by kim-em • Draft
2
perf: simple uniqueness analysis toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13180 opened Mar 29, 2026 by hargoniX • Draft
4
fix: missing borrow annotations in Std.Internal.UV.System changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13172 opened Mar 28, 2026 by algebraic-dev • Queued
@algebraic-dev
2
experiment: incremental compilation for leanir 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
#13171 opened Mar 28, 2026 by Kha • Draft
6
experiment: leanir Lake job prototype 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
#13169 opened Mar 28, 2026 by Kha • Draft
10
GetElemV draft
#13168 opened Mar 28, 2026 by datokrat • Draft
2
perf: introduce thread local reference type for StateRefT toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13165 opened Mar 28, 2026 by Rob23oba • Draft
4
ProTip! Updated in the last three days: updated:>2026-03-28.