Skip to content

Pull requests: leanprover/lean4

New pull request New
447 Open 9,372 Closed
447 Open 9,372 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: add high priority to OfSemiring.Q instances 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
#12782 opened Mar 4, 2026 by leodemoura Loading…
1
refactor: port EmitC to LCNF 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
#12781 opened Mar 3, 2026 by hargoniX • Draft
5
chore: nix shell: add python3 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…
2
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
test performance implications of implicit_reducible
#12761 opened Mar 2, 2026 by datokrat • Draft
2
proof of concept: Id defeq abuse linter
#12758 opened Mar 1, 2026 by datokrat • Draft
fix: mark Id.run as [implicit_reducible] 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
#12757 opened Mar 1, 2026 by leodemoura Loading…
3
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
20
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
fix: kernel: move level parameter count and thm-is-prop checks for robustness changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12734 opened Feb 28, 2026 by Copilot AI Loading…
1
@nomeata
14
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
6
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
feat: standalone List.extract lemmas, don't normalize extract into drop/take changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12703 opened Feb 26, 2026 by datokrat • Draft
2
feat: add structured TraceResult to TraceData changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12698 opened Feb 26, 2026 by kim-em Loading…
8
feat: add cslib package template toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12679 opened Feb 24, 2026 by Shreyas4991 • Draft
1
2
feat: leading whitespace on first token 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
#12662 opened Feb 23, 2026 by mhuisi Loading…
12
fix: detect native c++ stdlib instead of hard-coding for darwin toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12659 opened Feb 23, 2026 by jacobly0 • Draft
1
2
perf: persist grind preprocessing caches across calls changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12657 opened Feb 23, 2026 by sgraf812 • Draft
2 tasks done
4
ProTip! Mix and match filters to narrow down what you’re looking for.