Skip to content

Pull requests: leanprover/lean4

New pull request New
646 Open 11,086 Closed
646 Open 11,086 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: ctor size limit checking changelog-compiler Compiler, runtime, and FFI
#15075 opened Sep 8, 2026 by hargoniX Member • Queued
1
chore: stop creating lean-pr-testing-* branches in reference manual toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15074 opened Sep 8, 2026 by Garmelon Contributor Loading…
2
chore: LinearOrderPackage Nat changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15071 opened Sep 8, 2026 by TwoFX Member Loading…
2
feat: ChoiceResolutionInfo 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-no Do not include this PR in the release changelog 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
#15070 opened Sep 8, 2026 by mhuisi Contributor Loading…
4
feat: linearity markers for Vector changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15069 opened Sep 8, 2026 by hargoniX Member • Queued
2
fix: keep Info of elaborations that pass a hole through 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-no Do not include this PR in the release changelog 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
#15068 opened Sep 8, 2026 by mhuisi Contributor Loading…
6
feat: frame the exception channel changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15067 opened Sep 8, 2026 by sgraf812 Contributor • Draft
2
feat: virtual one-field structures 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 changelog-language Language features and metaprograms 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
#15066 opened Sep 8, 2026 by datokrat Contributor • Draft
3
feat: rewrite the Verso docstring parser to produce accurate syntax breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features and metaprograms 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
#15064 opened Sep 8, 2026 by david-christiansen Contributor Loading…
3
fix: update to mimalloc 3.4.5 backport releases/v4.34.0 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-no Do not include this PR in the release changelog 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
#15060 opened Sep 8, 2026 by Kha Member Loading…
4
feat: separator-preserving Syntax.identComponents? 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-no Do not include this PR in the release changelog 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
#15057 opened Sep 8, 2026 by mhuisi Contributor Loading…
4
feat: linearity marker for HashMaps 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
#15049 opened Sep 7, 2026 by hargoniX Member Loading…
12
feat: bundle the lean4lean external checker with release toolchains 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-other 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
#15048 opened Sep 6, 2026 by Kha Member • Draft
1 task
3
perf: mark thunk results as multi-threaded only when the thunk is builds-manual CI has verified that the Lean Language Reference builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15047 opened Sep 6, 2026 by Kha Member • Draft
4
fix: dependency order when rebuilding have telescopes in Sym.simp toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15046 opened Sep 6, 2026 by emerardd Loading…
1
2
fix: log goalsAccomplished for theorems generated using elab (#15044) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15045 opened Sep 6, 2026 by medovina Loading…
1
2
fix: add braces around the operator || with lower precedence, make regex portable toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15040 opened Sep 5, 2026 by yurivict Loading…
2
perf: compile the reference-counted deletion machinery with mimalloc toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15032 opened Sep 4, 2026 by Kha Member • Draft
4
perf: let Lean's allocations skip mimalloc's free-list scrub toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15031 opened Sep 4, 2026 by Kha Member • Draft
4
chore: remove redundant sepBy1 in subst parser builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-no Do not include this PR in the release changelog downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15029 opened Sep 4, 2026 by mhuisi Contributor Loading…
3
perf: move ref into the Core.Context cold subobject builds-manual CI has verified that the Lean Language Reference builds against this PR downstream-force Force creation of a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15027 opened Sep 4, 2026 by Kha Member • Draft
5
fix: keep the space before a hygieneInfo antiquotation builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-no Do not include this PR in the release changelog downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15025 opened Sep 4, 2026 by mhuisi Contributor Loading…
3
feat: add Float.fma and Float32.fma with logical model awaiting-author Waiting for PR author to address issues toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15024 opened Sep 4, 2026 by gaetanserre • Draft
3
feat: make Quot live in Sort (max 1 u) rather than Sort u 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
#15023 opened Sep 4, 2026 by arthur-adjedj Contributor • Draft
2
feat: verify the GMP-free bignum core against a Lean model changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15022 opened Sep 4, 2026 by Kha Member Loading…
2
ProTip! What’s not been updated in a month: updated:<2026-08-08.