Skip to content

Pull requests: leanprover/lean4

New pull request New
559 Open 10,241 Closed
559 Open 10,241 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

refactor: unify the mvcgen' spec apply path changelog-tactics User facing tactics
#14081 opened Jun 16, 2026 by sgraf812 Contributor • Draft
feat: extract WP superclass from WPMonad changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14080 opened Jun 16, 2026 by sgraf812 Contributor • Draft
4
feat: Float.Model changelog-library Library release-ci Enable all CI checks for a PR, like is done for releases
#14079 opened Jun 16, 2026 by TwoFX Member Loading…
test: reuse snapshots of most common headers across elab pile 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
#14077 opened Jun 16, 2026 by Kha Member • Draft
2
step 1 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14074 opened Jun 16, 2026 by hargoniX Contributor • Draft
4
test: add regression test for #13512 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14070 opened Jun 16, 2026 by TWal Contributor Loading…
3
chore: re-land "feat: expire idle task pool threads after 5 seconds (#14043)" 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
#14069 opened Jun 16, 2026 by Kha Member • Draft
2
feat: introduce Std.Async.TCP.SSL changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14066 opened Jun 16, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: introduce Std.Internal.SSL.Session changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14065 opened Jun 16, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: introduce Std.Internal.SSL.Context changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14064 opened Jun 16, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
fix: complete bodyless HTTP responses on the client instead of stalling changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14062 opened Jun 15, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: add Body.Stream error handling changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14059 opened Jun 15, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: wide fixed-width integer load/store accessors on ByteArray changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14053 opened Jun 15, 2026 by kim-em Collaborator • Draft
2
feat: add support for Nat.log2 in simp and cbv 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
#14047 opened Jun 14, 2026 by Rob23oba Contributor Loading…
2
chore: rewrite some Fin theorems to use NeZero changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14046 opened Jun 14, 2026 by plp127 Contributor Loading…
3
fix: panic in simp +ground congruence for class constructors toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14040 opened Jun 13, 2026 by mdbrnowski Contributor Loading…
1
2
doc: guide Claude to write concise inline comments 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
#14038 opened Jun 13, 2026 by kim-em Collaborator Loading…
2
feat: finalize libuv thread 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
#14037 opened Jun 12, 2026 by algebraic-dev Member • Draft
2
perf: outline heartbeat inc toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14035 opened Jun 12, 2026 by hargoniX Contributor • Draft
8
feat: add Triple.post_imp_elim and Triple.rotate_pre changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14034 opened Jun 12, 2026 by sgraf812 Contributor Loading…
2
perf: worst case n log n complexity for Array.qsort toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14033 opened Jun 12, 2026 by johanphenkel-cmd • Draft
1
@TwoFX
8
perf: parallel pre-read of import regions with --setup 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
#14032 opened Jun 12, 2026 by Kha Member Loading…
8
doc: fix typo in Format.bracketFill documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14018 opened Jun 11, 2026 by ia0 Loading…
2
doc: fix typo in Format.nest example toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14013 opened Jun 11, 2026 by ia0 Loading…
3
perf: avoid expensive instance re-synthesis in cbv changelog-language Language features and metaprograms
#14009 opened Jun 11, 2026 by wkrozowski Contributor • Draft
2
ProTip! Type g i on any issue or pull request to go back to the issue listing page.