Skip to content

Pull requests: leanprover/lean4

New pull request New
574 Open 10,070 Closed
574 Open 10,070 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

fix: respectTransparency (new mathlib) builds-mathlib CI has verified that Mathlib builds against this PR 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
#13895 opened May 29, 2026 by datokrat Contributor • Draft
2
feat: Void.get_mk builds-mathlib CI has verified that Mathlib builds against this PR 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
#13894 opened May 29, 2026 by tydeu Member • Draft
2
feat: control environment linters with Lean.Options changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13893 opened May 29, 2026 by wkrozowski Contributor • Draft
3
doc: remove duplicated sentence in decide docstring 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
#13892 opened May 29, 2026 by brettkoonce Loading…
4
feat: support serializing closures in CompactedRegion.save changelog-library Library 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
#13891 opened May 29, 2026 by Kha Member Loading…
4
refactor: move inductive information in compiler from lazily filled local caches to eager persistent environment extensions 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
#13882 opened May 29, 2026 by Kha Member Loading…
8
fix: isolate postponed in withSynthesize 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
#13876 opened May 28, 2026 by Rob23oba Contributor • Draft
1
2
test: lake: avoid git init in the checked-in test tree toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13873 opened May 28, 2026 by Kha Member Loading…
3
chore: CLAUDE.md: test failures that should be retried in stage 2 builds-manual CI has verified that the Lean Language Reference builds against this PR 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
#13871 opened May 28, 2026 by Kha Member Loading…
2
feat: add Environment.hasExposedBody helper changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13868 opened May 28, 2026 by kim-em Collaborator Loading…
4
chore: update release scripts toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13866 opened May 27, 2026 by Garmelon Contributor • Draft
2
feat: simp lemmas for LawfulApplicative 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
#13865 opened May 27, 2026 by frangio Loading…
3
feat: experimental cross-process jobserver via POSIX semaphore 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
#13856 opened May 26, 2026 by Kha Member • Draft
10
chore: remove USE_LAKE build option 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
#13855 opened May 26, 2026 by Kha Member • Draft
2
feat: add builtin linter sets and make linter.extra a builtin linter set builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms lake-ci Run all Lake tests 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
#13852 opened May 26, 2026 by wkrozowski Contributor Loading…
2
experiment: forbid large elim of recursive Prop inductives changelog-language Language features and metaprograms
#13851 opened May 26, 2026 by nomeata Collaborator • Draft
experiment: always check types for instance metavariables at instance… breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. 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
#13846 opened May 26, 2026 by TwoFX Member • Draft
2
refactor: format specifiers to align with Java/CLDR pattern language toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13845 opened May 25, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
experiment: always check types for instance metavariables at instance transparency 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
#13831 opened May 25, 2026 by TwoFX Member • Draft
2
feat: automatic try? suggestions for empty by, unsolved goals, and sorry 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
#13830 opened May 25, 2026 by nomeata Collaborator • Draft
3
perf: use SymM for bv_decide rewriting changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13827 opened May 24, 2026 by hargoniX Contributor • Draft
4
feat: improve handling of interrupt exceptions in the server 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
#13821 opened May 22, 2026 by Vtec234 Member • Draft
2
fix: app elaborator infotrees should have context when there is ambiguity 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
#13815 opened May 21, 2026 by kmill Collaborator Loading…
1
2
experiment: improved 'synthsized type class instance is not definitio… 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
#13814 opened May 21, 2026 by TwoFX Member • Draft
3
perf: Nat rep for boxed UInt64 / USize changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13810 opened May 21, 2026 by tydeu Member • Draft
4
ProTip! Mix and match filters to narrow down what you’re looking for.