Skip to content

Pull requests: leanprover/lean4

New pull request New
451 Open 9,344 Closed
451 Open 9,344 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: 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
3
feat: lemmas about step size iterators 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
2
feat: add Scan iterator combinator 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
2
fix: make sure AbstracNestedProofs.visit doesn't fail due to transparency issues 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
#12740 opened Feb 28, 2026 by arthur-adjedj Loading…
6
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…
3
guard LSP refresh requests behind capability check 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
3
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
chore: deprecate levelZero and levelOne toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12720 opened Feb 27, 2026 by kim-em Loading…
2
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 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
19
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
fix: validate stage0 version matches release version changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12700 opened Feb 26, 2026 by kim-em Loading…
1
6
feat: add structured TraceResult to TraceData 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 • Draft
4
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
perf: simplify cbv ite/dite simprocs by reducing Decidable instance directly changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12677 opened Feb 24, 2026 by wkrozowski Loading…
4
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…
6
feat: add ground evaluation for And/Or in Sym.Simp changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12660 opened Feb 23, 2026 by wkrozowski Loading…
4
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
chore: turn on new do elaborator in Core toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN unlock-upstream-stdlib-flags
#12656 opened Feb 23, 2026 by sgraf812 Loading…
28
experiment: fix various eta issues 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
#12636 opened Feb 21, 2026 by arthur-adjedj • Draft
1
19
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.