Skip to content

Pull requests: leanprover/lean4

New pull request New
576 Open 10,076 Closed
576 Open 10,076 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: recover theorem-backed grind? suggestions without regressing stable output changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13905 opened May 31, 2026 by peter941221 Loading…
4
perf: bump priority of Grind.IntModule.OfNatModule.ofNatModule 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
#13904 opened May 30, 2026 by hargoniX Contributor • Draft
6
feat: add HTTP Client changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13902 opened May 30, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: add RedirectPlan for validating and following redirects changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13901 opened May 30, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: add type class for replayable body types changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13900 opened May 30, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
perf: spawn child processes via libuv uv_spawn changelog-compiler Compiler, runtime, and FFI 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
#13898 opened May 30, 2026 by Kha Member • Draft
2
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
5
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
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
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 Contributor 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
ProTip! Filter pull requests by the default branch with base:master.