Skip to content

Pull requests: leanprover/lean4

New pull request New
543 Open 9,946 Closed
543 Open 9,946 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: remove redundant deprecation warnings changelog-language Language features and metaprograms
#13595 opened May 1, 2026 by wkrozowski Contributor • Draft
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
fix: remove @[expose] when unnecessary, fixing stage2 warnings in #13823 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
#13584 opened Apr 30, 2026 by datokrat Contributor Loading…
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 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
#13579 opened Apr 29, 2026 by Kha Member • Draft
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
fix: always fail on unsolved metavariables after Verso docstring elab changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13574 opened Apr 29, 2026 by david-christiansen Contributor Loading…
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
feat: add @[reducible_proj] for selective projection unfolding 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
#13562 opened Apr 29, 2026 by kim-em Collaborator • Draft
2
feat: make [defeq] attribute strict and stop auto-tagging := rfl breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13557 opened Apr 28, 2026 by nomeata Collaborator • Draft
2
[test] Rebase the respectTransparency.types changes 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
#13555 opened Apr 28, 2026 by datokrat Contributor • Draft
2
chore: increase priority of instSMulOfMul 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
#13554 opened Apr 28, 2026 by kim-em Collaborator • Draft
7
feat: more reliable dot notation and expected type propagation (experiment) 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
#13552 opened Apr 27, 2026 by kmill Collaborator • Draft
4
feat: better error messages and more complete logic for checkImpossibleInstance and checkNonClassInstance breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan force-mathlib-ci 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
#13550 opened Apr 27, 2026 by MoritzBeroRoos • Draft
6
fix: indicate in readModuleDataParts if memory is exhausted changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13549 opened Apr 27, 2026 by eric-wieser Contributor Loading…
4
fix: prevent corruption of the small allocator state changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13548 opened Apr 27, 2026 by eric-wieser Contributor Loading…
3
fix: propagate memory errors in mpz.cpp changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13547 opened Apr 27, 2026 by eric-wieser Contributor Loading…
3
perf: LLVM 19 -> 22 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13545 opened Apr 27, 2026 by hargoniX Contributor • Draft
4
ProTip! Mix and match filters to narrow down what you’re looking for.