Skip to content

Pull requests: leanprover/lean4

New pull request New
513 Open 9,816 Closed
513 Open 9,816 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: deriving Inhabited for structures should inherit Inhabited instances changelog-language Language features and metaprograms
#13395 opened Apr 13, 2026 by kmill Collaborator Loading…
1
feat: store eqn-affecting options at definition time instead of eager generation 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
#13394 opened Apr 13, 2026 by nomeata Collaborator Loading…
7
feat: add lake builtin-lint changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13393 opened Apr 13, 2026 by wkrozowski Contributor • Draft
2
fix: file read buffer overflow changelog-compiler Compiler, runtime, and FFI release-ci Enable all CI checks for a PR, like is done for releases
#13392 opened Apr 13, 2026 by hargoniX Contributor Loading…
1
10
fix: universe normalization in getDecLevel changelog-language Language features and metaprograms force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13391 opened Apr 13, 2026 by sgraf812 Contributor Loading…
3
feat: add instance validation checks in addInstance changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13389 opened Apr 13, 2026 by wkrozowski Contributor Loading…
2
perf: inline get_loose_bvar_range field accessor 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
#13387 opened Apr 13, 2026 by Kha Member • Draft
6
feat: allow attributes on structure fields toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13382 opened Apr 12, 2026 by SrGaabriel Loading…
1
2
perf: combined kernel optimizations 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
#13381 opened Apr 12, 2026 by Kha Member • Draft
13
perf: de-virtualize replace_rec_fn dispatch via templated functor toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13380 opened Apr 12, 2026 by Kha Member • Draft
4
perf: skip caching identity results in replace_rec_fn toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13379 opened Apr 12, 2026 by Kha Member • Draft
7
perf: small-buffer inline cache for replace_rec_fn toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13378 opened Apr 12, 2026 by Kha Member • Draft
4
perf: single-probe cache insert in replace_rec_fn toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13377 opened Apr 12, 2026 by Kha Member • Draft
4
perf: pre-reserve replace_rec_fn cache to avoid early rehashing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13376 opened Apr 12, 2026 by Kha Member • Draft
4
perf: skip kernel sharecommon on theorems toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13375 opened Apr 12, 2026 by Kha Member • Draft
8
chore: add missing noexcepts
#13370 opened Apr 10, 2026 by eric-wieser Contributor Loading…
feat: add type-correctness note to rewrite tactic error messages 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
#13368 opened Apr 10, 2026 by Kha Member • Draft
3
fix: prevent a hang in acLt 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
#13367 opened Apr 10, 2026 by eric-wieser Contributor Loading…
6
feat: use right-associativity in Level.max normalization breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13366 opened Apr 10, 2026 by kmill Collaborator • Draft
1
7
refactor: stop bumping transparency to .instances in whnfMatcher breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13363 opened Apr 10, 2026 by nomeata Collaborator • Draft
4
test toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13362 opened Apr 10, 2026 by hargoniX Contributor • Draft
8
fix: allow level assignments in wrapInstance 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
#13361 opened Apr 10, 2026 by JovanGerb Contributor Loading…
6
feat: add linter.redundantExpose for redundant @[expose]/@[no_expose] attributes 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
#13359 opened Apr 10, 2026 by Kha Member • Draft
4
proof of concept: simp lemmas spawing subgoals toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13358 opened Apr 10, 2026 by datokrat Contributor • Draft
2
fix: decLevel? should normalize breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13352 opened Apr 9, 2026 by kmill Collaborator • Draft
7
ProTip! Follow long discussions with comments:>50.