Skip to content

Pull requests: leanprover/lean4

New pull request New
617 Open 11,052 Closed
617 Open 11,052 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: expose Array.mapM for kernel reduction toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14996 opened Sep 2, 2026 by kim-em Collaborator Loading…
2
fix: require the Lake cache key rather than inferring secret availability 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
#14994 opened Sep 2, 2026 by kim-em Collaborator Loading…
2
fix: make the stack overflow handler async-signal-safe toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14993 opened Sep 1, 2026 by bbarwik Loading…
1
2
feat: add lake check to check a project against external checkers breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14990 opened Sep 1, 2026 by Kha Member Loading…
4
fix: expose Array.ofFn for kernel reduction builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14989 opened Sep 1, 2026 by kim-em Collaborator Loading…
2
fix: expose Vector DecidableEq for kernel reduction builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14988 opened Sep 1, 2026 by kim-em Collaborator Loading…
2
perf: cache the elaboration of section variables across commands 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
#14983 opened Sep 1, 2026 by marcelolynch Contributor • Draft
4
perf: heartbeat and theap in one thread-local 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
#14982 opened Aug 31, 2026 by TwoFX Member • Draft
9
perf: fuse heartbeat update into the small-object allocation call 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
#14981 opened Aug 31, 2026 by TwoFX Member • Draft
6
perf: do not include scalar children in mark_mt/mark_persistent 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
#14980 opened Aug 31, 2026 by TwoFX Member • Draft
4
perf: derive array capacity from mi_usable_size 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
#14979 opened Aug 31, 2026 by TwoFX Member • Draft
5
fix: correct Emscripten UV stub signatures toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14974 opened Aug 30, 2026 by mizchi Loading…
1
2
perf: give currRecDepth its own ReaderT layer in CoreM 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 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
#14970 opened Aug 29, 2026 by Kha Member • Draft
9
perf: cache the innermost scope state in ScopedEnvExtension.StateStack 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 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
#14968 opened Aug 29, 2026 by Kha Member • Draft
7
perf: move currRecDepth from Core.Context into Core.State toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14966 opened Aug 29, 2026 by Kha Member • Draft
4
fix: kernel error from simp results cached with a proof that has free variables 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
#14965 opened Aug 29, 2026 by nomeata Collaborator • Draft
1
3
fix: deriving ToJson/FromJson for mutual groups with self-recursion toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14959 opened Aug 28, 2026 by rish987 Contributor Loading…
1
2
chore: remove unreachable case in LCNF.checkMeta 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
#14955 opened Aug 28, 2026 by Kha Member • Draft
2
perf: add a scalar fast path to lean_nat_shiftl toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14954 opened Aug 28, 2026 by Timeroot Contributor Loading…
6
doc: rewrite apply, exact, refine and refine' tactic docstrings toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14952 opened Aug 28, 2026 by Vierkantor Contributor Loading…
3
experiment: allocation logic and mimalloc in one TU toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14950 opened Aug 28, 2026 by TwoFX Member • Draft
12
feat: mutual inductives with multiple universes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14945 opened Aug 27, 2026 by Timeroot Contributor • Draft
2
feat: allow optParam and autoParam in implicit binders 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
#14942 opened Aug 27, 2026 by Kha Member • Draft
3
[Backport releases/v4.34.0] chore: update to mimalloc 3.4.4
#14938 opened Aug 27, 2026 by github-actions Bot Loading…
feat: add Html 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 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
#14935 opened Aug 27, 2026 by Vtec234 Member • Draft
9
ProTip! Follow long discussions with comments:>50.