Skip to content

Pull requests: leanprover/lean4

New pull request New
585 Open 10,644 Closed
585 Open 10,644 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

perf: avoid escaping ModuleRefs keys 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 needs-update-stage0 stage 0 should be updated after merging this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14465 opened Jul 20, 2026 by Vtec234 Member Loading…
4
chore: rename Nat.div_eq to Nat.div_eq_ite 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-library Library 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
#14462 opened Jul 20, 2026 by TwoFX Member Loading…
3
chore: make file_not_found test more robust changelog-no Do not include this PR in the release changelog 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
#14461 opened Jul 20, 2026 by TwoFX Member Loading…
2
perf: skip re-attempting pending TC mvars with unchanged instantiated goals (quadratic resumption, #14448) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14449 opened Jul 19, 2026 by grandchildrice Loading…
2
feat: forbid non-reserved identifiers via withForbidden 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
#14432 opened Jul 17, 2026 by sgraf812 Contributor Loading…
5
fix: vcgen [f] unfolding of definitions by root match changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14429 opened Jul 17, 2026 by sgraf812 Contributor Loading…
4
feat: warn on transitive deprecations 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 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
#14422 opened Jul 16, 2026 by wkrozowski Contributor • Draft
2
feat: look for .ilean.mmap files on watchdog load 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
#14421 opened Jul 16, 2026 by robsimmons Contributor Loading…
2
feat: add @[trusted_axiom] attribute and linter.untrustedAxioms linter 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
#14407 opened Jul 16, 2026 by Kha Member Loading…
8
feat: support code actions in linters 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
#14402 opened Jul 15, 2026 by wkrozowski Contributor Loading…
4
feat: support join points in vcgen via synthetic backward rules changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14398 opened Jul 15, 2026 by sgraf812 Contributor • Draft
2
fix: make replay output a kernel environment changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14391 opened Jul 14, 2026 by hanwenzhu Contributor Loading…
1
3
feat: intrinsic verification syntax for do-notation loops and def contracts changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14389 opened Jul 14, 2026 by sgraf812 Contributor • Draft
2
doc: add blank line after list in omega docstring toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14381 opened Jul 14, 2026 by ia0 Contributor Loading…
2
refactor: lake: parse string slices 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
#14374 opened Jul 13, 2026 by tydeu Member • Draft
2
perf: normalize free variables in the type class resolution cache key 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
#14369 opened Jul 12, 2026 by Kha Member • Draft
4
perf: store per-module constant prefix trees in oleans 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
#14362 opened Jul 11, 2026 by Kha Member • Draft
64
fix: align Lean/Level.lean and kernel/level.cpp normalization rules changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14356 opened Jul 10, 2026 by digama0 Collaborator Loading…
2
perf: run isDefEqOnFailure only once per failing isDefEq 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
#14351 opened Jul 10, 2026 by datokrat Contributor • Draft
4
fix: enforce set notation per-element indentation 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
#14350 opened Jul 10, 2026 by Kha Member Loading…
4
refactor: split registerParametricAttribute into extension creation and registration 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-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
#14344 opened Jul 9, 2026 by wkrozowski Contributor Loading…
2
[REBASED] experiment: consolidate all TC opts 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
#14339 opened Jul 9, 2026 by Kha Member • Draft
28
feat: test for #9420 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
#14332 opened Jul 9, 2026 by Vtec234 Member • Draft
2
perf: memoize stuck type class resolution queries 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
#14327 opened Jul 8, 2026 by Kha Member • Draft
8
fix: load missing dynlibs individually with precompileModules and initialize lazily 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-lake Lake force-mathlib-ci macos-arm-ci Build for darwin_aarch64 in CI 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
#14326 opened Jul 8, 2026 by Vtec234 Member Loading…
2
ProTip! Type g i on any issue or pull request to go back to the issue listing page.