Skip to content

Pull requests: leanprover/lean4

New pull request New
450 Open 9,400 Closed
450 Open 9,400 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

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…
[Backport releases/v4.29.0] fix: remove @[grind →] from getElem_of_getElem?
#12823 opened Mar 6, 2026 by github-actions bot Loading…
feat: bundle leantar with Lean 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 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
#12822 opened Mar 6, 2026 by tydeu Loading…
3
fix: prevent cbv from picking up classical Decidable instances changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12816 opened Mar 5, 2026 by wkrozowski • Draft
10
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
fix: type mismatches in cbv proof terms about ite/dite/Decide changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12811 opened Mar 5, 2026 by wkrozowski Loading…
6
chore: migrate more tests to new test suite 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
#12809 opened Mar 5, 2026 by Garmelon Loading…
2
test: add instantiateMVars tests and benchmark for delayed assignments 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
#12808 opened Mar 5, 2026 by nomeata Loading…
6
feat: track persistently which declarations are simple ground 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
#12806 opened Mar 5, 2026 by hargoniX Loading…
6
feat: add grind.unusedLemmaThreshold option to report unused E-matching activations 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
#12805 opened Mar 5, 2026 by kim-em Loading…
6
refactor: port EmitC to LCNF 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
#12781 opened Mar 3, 2026 by hargoniX • Draft
7
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
fix: improve Name.isMetaprogramming changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12767 opened Mar 2, 2026 by JovanGerb 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
chore: CI: bump actions/upload-artifact from 5 to 7 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
#12752 opened Mar 1, 2026 by dependabot bot Loading…
2
chore: CI: bump actions/download-artifact from 7 to 8 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
#12751 opened Mar 1, 2026 by dependabot bot Loading…
2
chore: CI: bump dawidd6/action-download-artifact from 11 to 16 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
#12750 opened Mar 1, 2026 by dependabot bot Loading…
2
feat: use terminology "non-recursive structure" instead of "struct-like" changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12749 opened Mar 1, 2026 by kmill Loading…
1
4
feat: lemmas about step size iterators changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12748 opened Mar 1, 2026 by datokrat • Draft
4
feat: add Scan iterator combinator changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12742 opened Mar 1, 2026 by cmlsharp Loading…
1
23
fix: notify LSP client when worker process crashes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12736 opened Feb 28, 2026 by wvhulle Loading…
4
fix: guard LSP refresh requests behind capability check changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12735 opened Feb 28, 2026 by wvhulle Loading…
1
4
feat: XID support in Lean identifiers toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12726 opened Feb 27, 2026 by hargoniX • Draft
11
feat: generalize below and brecOn on subsingletons 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 P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12718 opened Feb 26, 2026 by arthur-adjedj Loading…
1
20
ProTip! Add no:assignee to see everything that’s not assigned.