Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings

Pull requests: leanprover/lean4

New pull request New
364 Open 8,604 Closed
364 Open 8,604 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: add Sym.getMaxFVar? changelog-library Library
#11794 opened Dec 25, 2025 by leodemoura • Queued
feat: enable disjunctive side-conditions of grind_pattern changelog-feat toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11791 opened Dec 24, 2025 by pirapira • Draft
1
3
feat: @[allow_native_decide] kernel check changelog-language Language features and metaprograms
#11790 opened Dec 24, 2025 by Kha • Draft
feat: make FinitenessRelation public API breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#11789 opened Dec 24, 2025 by datokrat • Draft
2
fix: pretty-printing of unification hints awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11780 opened Dec 23, 2025 by grunweg Loading…
3
fix: add missing .ofNats in lake translate-config changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11771 opened Dec 22, 2025 by eric-wieser Loading…
3
feat: replace range_succ by range_add_one 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
#11768 opened Dec 22, 2025 by JovanGerb Loading…
2
feat: cons_eliminator 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
#11767 opened Dec 22, 2025 by tobiasgrosser • Draft
5
feat: add guards for grind patterns for getElem?_eq_none theorems 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
#11761 opened Dec 21, 2025 by kim-em Loading…
2
refactor: common infrastructure for realizable theorems 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
#11757 opened Dec 21, 2025 by nomeata • Draft
2
perf: JsonNumber comparison no longer eagerly aligns mantissa builds-manual CI has verified that the Lean Language Reference builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11750 opened Dec 20, 2025 by JasonGross • Draft
2
fix: disable order and funCC modules in NoopConfig awaiting-mathlib We should not merge this until we have a successful Mathlib build 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
#11744 opened Dec 20, 2025 by kim-em Loading…
2
perf: use absl::flat_hash_map
#11743 opened Dec 19, 2025 by Kha • Draft
2
feat: add claude tactic for AI-assisted proof suggestions 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
#11741 opened Dec 19, 2025 by kim-em • Draft
2
test: benchmark engine_let_forall_exists_and.lean toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11740 opened Dec 19, 2025 by andres-erbsen • Draft
4
chore: improve unexpected token messages toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11725 opened Dec 18, 2025 by alok Loading…
3
fix: Signal.Handler segmentation fault with Selector changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11724 opened Dec 18, 2025 by algebraic-dev Loading…
@algebraic-dev
2
feat: add Std.Future to enable IO.Promise-like behavior in Selectable contexts changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11723 opened Dec 17, 2025 by algebraic-dev Loading…
@algebraic-dev
2
perf: match equations: use diteInduction to split 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
#11720 opened Dec 17, 2025 by nomeata • Draft
13
perf: match compilation: pick out overlap assumption directly 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 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
#11711 opened Dec 17, 2025 by nomeata • Draft
5
feat: a grind configuration for use in match equation compilation changelog-language Language features and metaprograms
#11703 opened Dec 16, 2025 by nomeata • Draft
refactor: move error explanation text to the manual 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
#11688 opened Dec 15, 2025 by robsimmons Loading…
2
fix: add missing pp-spaces in grind_pattern toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11686 opened Dec 15, 2025 by adomani • Draft
3
feat: lake: multi-version workspaces breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-lake Lake 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
#11662 opened Dec 14, 2025 by tydeu • Draft
4
chore: add missing .run and .mks in monad transformers
#11647 opened Dec 13, 2025 by eric-wieser • Draft
ProTip! Adding no:label will show everything without a label.
Morty Proxy This is a proxified and sanitized view of the page, visit original site.