Skip to content

Pull requests: leanprover/lean4

New pull request New
620 Open 10,999 Closed
620 Open 10,999 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

feat: lake: read persisted code quality entries in lake lint --code-quality changelog-lake Lake
#14933 opened Aug 26, 2026 by wkrozowski Contributor Loading…
perf: restrict and record option accesses during type class resolution
#14932 opened Aug 26, 2026 by Kha Member • Draft
4
feat: new deriving handlers for BEq, Ord, ReflBEq and ReflOrd toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14929 opened Aug 25, 2026 by Rob23oba Contributor • Draft
2
perf: try eta-expansion before delta-reduction in the kernel 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
#14927 opened Aug 25, 2026 by Kha Member • Draft
1
6
feat: allow disabling termination warnings when using addPreDefinitions 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
#14912 opened Aug 24, 2026 by Rob23oba Contributor Loading…
2
test: complete no-concurrency Lean model of refcounting
#14910 opened Aug 24, 2026 by Kha Member Loading…
perf: count only user-mode instructions in benchmarks 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
#14908 opened Aug 24, 2026 by Kha Member • Draft
4
feat: lake: separate leanir job changelog-lake Lake
#14906 opened Aug 24, 2026 by tydeu Member • Draft
fix: make theorems opaque to the kernel as well 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
#14896 opened Aug 23, 2026 by nomeata Collaborator • Draft
7
feat: drop the universe bump from PSigma, PProd and PULift changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14893 opened Aug 22, 2026 by nomeata Collaborator • Draft
7
feat: define well-founded recursion without large elimination of Acc 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
#14892 opened Aug 22, 2026 by nomeata Collaborator • Draft
2
test: how costly is eta-for-unit ? 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 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
#14891 opened Aug 22, 2026 by arthur-adjedj Contributor • Draft
18
fix(Data/Dyadic): swap names of Dyadic.not_lt and Dyadic.not_le P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14890 opened Aug 22, 2026 by plp127 Contributor Loading…
2
feat: add lake check as a comparator frontend breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-lake Lake 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
#14885 opened Aug 21, 2026 by Kha Member • Draft
2
feat: introduce findMatchingDecl? for code quality checks wrapped in Lean.Linter (DRAFT) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14880 opened Aug 21, 2026 by wkrozowski Contributor • Draft
2
chore: update to mimalloc 3.5.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 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
#14866 opened Aug 20, 2026 by Kha Member • Draft
4
fix: adjust name mangling in kernel's nested inductive type processing 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
#14846 opened Aug 19, 2026 by kmill Collaborator • Draft
1
2
refactor: new LRAT checker
#14842 opened Aug 19, 2026 by hargoniX Member • Draft
22
fix: reuse the instances of a non-exposed definition in inferInstanceAs 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
#14840 opened Aug 19, 2026 by gasparattila Loading…
1
3
feat: lake: make job cancellation a first-class JobState flag builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14835 opened Aug 19, 2026 by dennj Contributor Loading…
5
refactor: derive vcgen's exception postcondition rules from a type class changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14827 opened Aug 18, 2026 by sgraf812 Contributor • Draft
4
fix: better structural recursion equations 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
#14822 opened Aug 18, 2026 by Rob23oba Contributor • Draft
6
linear probing experiment toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14810 opened Aug 18, 2026 by TwoFX Member • Draft
8
perf: special case single-child nodes in DiscrTree 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
#14805 opened Aug 17, 2026 by robsimmons Contributor • Draft
13
fix: refcounting and error reporting in the libuv bindings 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
#14796 opened Aug 15, 2026 by algebraic-dev Member • 1/4 Loading…
3
ProTip! What’s not been updated in a month: updated:<2026-07-26.