Skip to content

Pull requests: leanprover/lean4

New pull request New
549 Open 9,971 Closed
549 Open 9,971 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

feat: split [implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers changelog-language Language features and metaprograms
#13637 opened May 5, 2026 by kim-em Collaborator Loading…
feat: restrict simpa using h close to reducible transparency changelog-tactics User facing tactics
#13636 opened May 5, 2026 by kim-em Collaborator Loading…
chore: use the lean-llvm LLVM for benchmarking toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13634 opened May 4, 2026 by hargoniX Contributor Loading…
20
fix: withoutExporting around diagnostic reporting changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13630 opened May 4, 2026 by kim-em Collaborator Loading…
1
2
feat: add @[attribute] for registering custom attributes 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
#13629 opened May 4, 2026 by Kha Member • Draft
4
fix: apply rcases substitution before recording pattern info changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13621 opened May 3, 2026 by berberman • Draft
1
4
fix: reject attribute uses whose module is reachable only via IR 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
#13613 opened May 2, 2026 by Kha Member • Draft
2
feat: expose fields required for implementing linters outside of Lean core with detailed auto-fixes and diagnostic tags toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13610 opened May 2, 2026 by wvhulle • Draft
2
chore: export function needed to implement dead / unused code detection functions outside of Lean core by users toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13609 opened May 2, 2026 by wvhulle • Draft
2
feat: show live Lake LSP loading progress in status bar of editors instead of top of file toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13608 opened May 2, 2026 by wvhulle • Draft
2
Nix flake improvements toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13607 opened May 2, 2026 by wvhulle • Draft
2
Lsp formatting toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13606 opened May 2, 2026 by wvhulle • Draft
2
feat: remove redundant deprecation warnings changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13595 opened May 1, 2026 by wkrozowski Contributor • Draft
2
feat: add values/valuesArray lemmas for (D)HashMap toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13594 opened May 1, 2026 by pandaman64 Contributor Loading…
2
refactor: use libuv for subprocesses 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
#13591 opened Apr 30, 2026 by eric-wieser Contributor • Draft
4
fix: perform severity overrides before counting errors changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13589 opened Apr 30, 2026 by eric-wieser Contributor Loading…
1
3
fix: kernel type mismatch in cutsat eq_def proofs changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13587 opened Apr 30, 2026 by leodemoura Member Loading…
1
2
feat: upstream unreachableTactic linter 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
#13580 opened Apr 29, 2026 by wkrozowski Contributor • Draft
2
fix: record instances unfolded by wrapInstance as shake dependencies backport releases/v4.30.0 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
#13579 opened Apr 29, 2026 by Kha Member Loading…
2
test: Bring Sym-based mvcgen' on par with mvcgen toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13578 opened Apr 29, 2026 by sgraf812 Contributor • Draft
6
fix: tail-recursive BitVec.ofBoolListLE/ofBoolListBE to avoid stack overflow toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13576 opened Apr 29, 2026 by kim-em Collaborator • Draft
2
feat: add Locale and LocaleSymbols for configurable date/time formatting changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13567 opened Apr 29, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
fix: correct off-by-one in toSeconds and wrong day count in Year.days changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13566 opened Apr 29, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
fix: prioritize TZ and TZDIR over /etc/localtime in TZDB search changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13565 opened Apr 29, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
chore: make Glob.ofString? public changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13563 opened Apr 29, 2026 by kim-em Collaborator Loading…
2
ProTip! Exclude everything labeled bug with -label:bug.