Skip to content

Pull requests: leanprover/lean4

New pull request New
447 Open 9,467 Closed
447 Open 9,467 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: use process signal numbers from correct architecture changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12900 opened Mar 12, 2026 by Garmelon • Draft
2
experiment: normalize all instances 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
#12899 opened Mar 12, 2026 by Kha • Draft
2
experiment: normalize instances from def deriving 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
#12897 opened Mar 12, 2026 by Kha • Draft
2
feat: add tracing to cbv 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
#12896 opened Mar 12, 2026 by wkrozowski Loading…
4
experiment: normalize instances in inferInstanceAs 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
#12895 opened Mar 12, 2026 by Kha • Draft
11
feat: make Nat.strongRecOn and Nat.caseStrongRecOn computable 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
#12894 opened Mar 12, 2026 by Parcly-Taxel Loading…
14
test: add mvcgen' with <tac> and mvcgen' with grind to sym-based VCGen toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12893 opened Mar 11, 2026 by sgraf812 • Draft
2
chore: mark Pure.pure as match_pattern toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12892 opened Mar 11, 2026 by eric-wieser Loading…
2
perf: optimize string literal equality simprocs for kernel efficiency builds-mathlib CI has verified that Mathlib builds against this PR changelog-tactics User facing tactics 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
#12887 opened Mar 11, 2026 by nomeata Loading…
5
chore: replace compareOfLessAndEq with compareOfLT
#12868 opened Mar 10, 2026 by astrainfinita • Draft
1
1
fix: handle lean4-nightly toolchain prefix in release checklist changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12865 opened Mar 10, 2026 by kim-em Loading…
2
feat: enable use of lamba term as motive in match toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12862 opened Mar 10, 2026 by goretkin • Draft
2
refactor: prepare for type family motives in match expressions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12861 opened Mar 10, 2026 by goretkin • Draft
2
feat: auto eta-expand structures in grind when equality with constructor is present builds-mathlib CI has verified that Mathlib builds against this PR changelog-tactics User facing tactics 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
#12860 opened Mar 10, 2026 by kim-em • Draft
6
perf: try letToHave for dependent lets in cbv changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12856 opened Mar 9, 2026 by wkrozowski • Draft
4
feat: defeqParam gadget for delayed assignment metavariables 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
#12854 opened Mar 9, 2026 by kmill • Draft
1
3
fix: namespace used in private import and current module vanishes dowstream 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
#12840 opened Mar 8, 2026 by Kha • Draft
1
5
perf: path compression for DiscrTree 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
#12838 opened Mar 7, 2026 by nomeata • Draft
13
feat: respect user provided borrow annotations toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12830 opened Mar 6, 2026 by hargoniX • Draft
4
feat: String.toNat? lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet.
#12828 opened Mar 6, 2026 by TwoFX • Draft
2
chore: grind guard condition for List.eq_or_mem_of_mem_cons awaiting-mathlib We should not merge this until we have a successful Mathlib build changelog-library Library
#12824 opened Mar 6, 2026 by kim-em Loading…
perf: improve proof-over-applied cases in ToLCNF builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI 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
#12814 opened Mar 5, 2026 by Rob23oba Loading…
4
chore: nix shell: add python314 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12774 opened Mar 3, 2026 by fiforeach Loading…
3
proof of concept: Id defeq abuse linter
#12758 opened Mar 1, 2026 by datokrat • Draft
chore: CI: bump actions/create-github-app-token from 2.0.2 to 2.2.1 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12753 opened Mar 1, 2026 by dependabot bot Loading…
2
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.