Skip to content

Pull requests: leanprover/lean4

New pull request New
544 Open 10,053 Closed
544 Open 10,053 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

perf: try to emit assumes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13732 opened May 14, 2026 by hargoniX Contributor • Draft
4
feat: add newDecls fields to Core.State and Command.State changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13731 opened May 14, 2026 by wkrozowski Contributor • Draft
7
experiment: reduce clangs cleverness toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13727 opened May 13, 2026 by hargoniX Contributor • Draft
4
feat: improve semantic highlighting (close #2305) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13726 opened May 13, 2026 by RIvance Loading…
1
2
[don’t merge] cherry-pick try-on-empty-by to v4.30rc2 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
#13724 opened May 13, 2026 by nomeata Collaborator • Draft
2
feat: proof mode for new foundations of mvcgen 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 changelog-library Library 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
#13722 opened May 13, 2026 by volodeyka Contributor Loading…
2
chore: CI: build everything with Lake 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
#13721 opened May 13, 2026 by Kha Member • Draft
6
perf: inline assorted declarations used in match_expr toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13716 opened May 12, 2026 by hargoniX Contributor • Draft
4
fix: do not block on async theorem bodies when iterating local consts 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 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
#13712 opened May 11, 2026 by nomeata Collaborator Loading…
1
4
restrict lazy WHNF to reducible (test) breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference 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
#13702 opened May 11, 2026 by datokrat Contributor • Draft
6
chore: re-enable LLVM CI 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 changes-stage0 Contains stage0 changes, merge manually using rebase 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
#13700 opened May 11, 2026 by hargoniX Contributor • Draft
22
feat: collect diagnostic explanations into hover popup
#13697 opened May 10, 2026 by wvhulle • Draft
feat: ship lsp-probe test-equipment binary toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13696 opened May 10, 2026 by wvhulle • Draft
2
fix: Expose related information diagnostics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13695 opened May 10, 2026 by wvhulle • Draft
2
feat: verifiable whileM via ordered fixpoints for stronger specs changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13689 opened May 8, 2026 by sgraf812 Contributor • Draft
2
feat: support mvcgen' inside sym => … blocks changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13680 opened May 7, 2026 by sgraf812 Contributor • Draft
2
fix: codegen should not inspect private ctor of public type breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI fast-ci Forces the use of large runners so that e.g. PR releases are created faster 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
#13679 opened May 7, 2026 by Kha Member Loading…
10
feat: more semantic tokens for Markdown/Verso changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13674 opened May 7, 2026 by david-christiansen Contributor Loading…
3
test 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
#13660 opened May 6, 2026 by datokrat Contributor • Draft
2
chore: rebase #13283 to nightly-with-mathlib 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
#13658 opened May 6, 2026 by datokrat Contributor • Draft
2
feat: add Dyadic.divAtPrec for round-down dyadic division at given precision 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 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
#13654 opened May 6, 2026 by kim-em Collaborator Loading…
1
2
feat: completions for user simp options changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13650 opened May 5, 2026 by kmill Collaborator • Draft
2
[Backport releases/v4.30.0] fix: record instances unfolded by wrapInstance as shake dependencies
#13648 opened May 5, 2026 by github-actions Bot Loading…
feat: add requiresModuleSystem package option in Lake 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
#13646 opened May 5, 2026 by Kha Member • Draft
2
feat: split [implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers 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 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
#13637 opened May 5, 2026 by kim-em Collaborator • Draft
2
ProTip! Adding no:label will show everything without a label.