Skip to content

Pull requests: leanprover/lean4

New pull request New
376 Open 8,632 Closed
376 Open 8,632 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: zetaDelta at Sym/Pattern.lean changelog-tactics User facing tactics
#11849 opened Dec 30, 2025 by leodemoura • Queued
chore: backtick identifiers in core messages and tests
#11846 opened Dec 30, 2025 by alok • Draft
chore: backtick identifiers in Lake eval messages toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11845 opened Dec 30, 2025 by alok • Draft
2
chore: backtick identifiers in do-tactic attribute messages toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11844 opened Dec 30, 2025 by alok • Draft
2
chore: backtick identifiers in delaborator messages toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11843 opened Dec 30, 2025 by alok • Draft
2
chore: backtick identifiers in meta tactic messages
#11842 opened Dec 30, 2025 by alok • Draft
chore: backtick identifiers in Ext/Simpa messages toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11841 opened Dec 30, 2025 by alok • Draft
2
chore: backtick identifiers in elaborator tactic messages
#11840 opened Dec 30, 2025 by alok • Draft
chore: backtick identifiers in compiler diagnostics
#11839 opened Dec 30, 2025 by alok • Draft
perf: use Array for CNF formulas
#11832 opened Dec 29, 2025 by hargoniX • Draft
2
feat: increase number of constructors
#11831 opened Dec 29, 2025 by tobiasgrosser • Draft
1
perf: test uniqueness non-atomically first in lean_dec_ref_cold 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
#11830 opened Dec 29, 2025 by Kha • Draft
4
perf: outline lean_dec_ref_cold deletion case
#11829 opened Dec 29, 2025 by Kha • Draft
4
feat: suggest guillemet escaping in parser error
#11822 opened Dec 28, 2025 by alok • Draft
fix: add mem_eraseDups lemma for List deduplication changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11811 opened Dec 27, 2025 by NicolasRouquette Loading…
1
6
fix: add missing dependencies for copy-leancpp target toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11809 opened Dec 27, 2025 by NicolasRouquette Loading…
1
3
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
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…
4
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
ProTip! Type g i on any issue or pull request to go back to the issue listing page.