Skip to content

Pull requests: leanprover/lean4

New pull request New
582 Open 10,341 Closed
582 Open 10,341 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: fix vcgen frames feature for monads with multiple StateT transformers toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14217 opened Jun 29, 2026 by volodeyka Contributor • Draft
2
chore: make Nat.ne_of_gt protected changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14216 opened Jun 29, 2026 by b-mehta Contributor • Queued
3
refactor: port bv_decide reflection to SymM changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14215 opened Jun 29, 2026 by hargoniX Contributor • Draft
6
doc: improve error message for unknown attributes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14213 opened Jun 29, 2026 by 0rca Loading…
1
2
feat: add List.Nodup.length_le_of_subset 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
#14212 opened Jun 29, 2026 by kim-em Collaborator Loading…
2
feat: add List.perm_ext_iff_of_nodup 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
#14211 opened Jun 29, 2026 by kim-em Collaborator Loading…
3
feat: add idxOf/getElem round-trip lemmas 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
#14210 opened Jun 29, 2026 by kim-em Collaborator Loading…
3
perf: compile Bool.not and Bool.toNat without branches toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14207 opened Jun 29, 2026 by JJYYY-JJY Loading…
6
feat: use linter framework for deferred docstring checks changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14206 opened Jun 28, 2026 by david-christiansen Contributor Loading…
2
fix: detect failures when flushing module oleans toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14204 opened Jun 28, 2026 by eric-wieser Contributor • Draft
2
chore: delete unused C++ code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14203 opened Jun 28, 2026 by eric-wieser Contributor Loading…
4
feat: track libuv request refs to support thread finalization changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14202 opened Jun 27, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
fix: generalize equality @[spec] rules over their explicit arguments changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14197 opened Jun 26, 2026 by sgraf812 Contributor • Draft
2
feat: clarify warning for semireducible definitions of class type 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
#14196 opened Jun 26, 2026 by datokrat Contributor • Draft
2
feat: extensible frame inference for vcgen via @[frameproc] changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14195 opened Jun 26, 2026 by sgraf812 Contributor • Draft
2
perf: optimize ToJson derive handler 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
#14186 opened Jun 25, 2026 by Kha Member • Draft
4
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…
6
[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
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
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.