Skip to content

Pull requests: leanprover/lean4

New pull request New
573 Open 10,322 Closed
573 Open 10,322 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 test snapshots opt-in toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14188 opened Jun 25, 2026 by Kha Member • Queued
2
perf: avoid proof wait in addEMatchAttr 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
#14187 opened Jun 25, 2026 by Kha Member Loading…
3
perf: optimize ToJson derive handler 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
#14186 opened Jun 25, 2026 by Kha Member • Draft
3
perf: avoid spawning a new thread per worker output message toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14185 opened Jun 25, 2026 by Kha Member Loading…
4
feat: lean_set_initializing 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-ffi 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
#14184 opened Jun 25, 2026 by tydeu Member Loading…
4
perf: make findIdx e-matching less aggressive 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
#14182 opened Jun 25, 2026 by hargoniX Contributor • Draft
4
[DO NOT MERGE] Backport incremental snapshots to v4.28 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14179 opened Jun 25, 2026 by Kha Member • Draft
perf: less aggressive {List,Array}.count e-matching breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#14177 opened Jun 25, 2026 by hargoniX Contributor Loading…
9
chore: Claude: document the CI stage2 trigger in the stage2-olean-test skill 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
#14176 opened Jun 25, 2026 by Kha Member Loading…
2
fix: repair dead lean-manual:// links (Closes #14163) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14171 opened Jun 24, 2026 by attilavjda Loading…
1
4
chore: test adaptation PR CI builds-mathlib CI has verified that Mathlib builds against this PR downstream Request a downstream-lean4 adaptation 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
#14170 opened Jun 24, 2026 by Garmelon Contributor • Draft
3
fix: make Hoare Triple universe-polymorphic in its assertion type 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
#14168 opened Jun 24, 2026 by sgraf812 Contributor • Draft
2
fix: reject stale incremental snapshot imports changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14166 opened Jun 24, 2026 by eluvane Contributor Loading…
3
fix: avoid recursive object compaction changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14165 opened Jun 24, 2026 by eluvane Contributor Loading…
7
feat: ThreadSanitizer support 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
#14161 opened Jun 23, 2026 by hargoniX Contributor • Draft
2
feat: labeled return, break, and continue in do notation changelog-language Language features and metaprograms
#14160 opened Jun 23, 2026 by sgraf812 Contributor • Draft
1
feat: add ByteArray.copyWithin changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14158 opened Jun 23, 2026 by kim-em Collaborator • Draft
6
feat: add collectAxiomsMany for batched axiom collection changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14157 opened Jun 23, 2026 by kim-em Collaborator Loading…
2
feat: add Insert instances for NameMap/NameSet 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-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
#14153 opened Jun 22, 2026 by Vtec234 Member Loading…
2
chore: remove custom small allocator changelog-no Do not include this PR in the release changelog 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
#14149 opened Jun 22, 2026 by hargoniX Contributor Loading…
2
perf: lazy IR loading 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
#14145 opened Jun 22, 2026 by Kha Member • Draft
12
hbv/json gerät++
#14144 opened Jun 22, 2026 by hargoniX Contributor • Draft
2
chore: disable binary stripping in release configuration builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI 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
#14139 opened Jun 22, 2026 by hargoniX Contributor Loading…
4
perf: short-circuit Sym pattern matching on pointer equality changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14137 opened Jun 22, 2026 by sgraf812 Contributor • Draft
2
fix: split universe levels for le_of_forall_le lemma changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14133 opened Jun 21, 2026 by volodeyka Contributor • Draft
3
ProTip! Mix and match filters to narrow down what you’re looking for.