Skip to content

Pull requests: leanprover/lean4

New pull request New
381 Open 8,645 Closed
381 Open 8,645 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

style: fix doubled word in Lake docstring toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11867 opened Jan 1, 2026 by alok Loading…
2
style: fix spelling errors in Lean/ docstrings toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11865 opened Jan 1, 2026 by alok Loading…
2
style: fix doubled words in Init/ and Std/ docstrings toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11864 opened Jan 1, 2026 by alok Loading…
2
chore: CI: bump actions/download-artifact from 6 to 7 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11863 opened Jan 1, 2026 by dependabot bot Loading…
2
chore: CI: bump actions/cache from 4 to 5 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11862 opened Jan 1, 2026 by dependabot bot Loading…
2
fix: add OfNat instance for LeanOptionValue changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11859 opened Jan 1, 2026 by eric-wieser Loading…
3
chore: backtick identifiers in core messages and tests
#11846 opened Dec 30, 2025 by alok Loading…
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 Loading…
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 Loading…
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 Loading…
2
chore: backtick identifiers in meta tactic messages
#11842 opened Dec 30, 2025 by alok Loading…
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 Loading…
2
chore: backtick identifiers in elaborator tactic messages 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
#11840 opened Dec 30, 2025 by alok Loading…
2
chore: backtick identifiers in compiler diagnostics breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11839 opened Dec 30, 2025 by alok Loading…
2
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…
5
ProTip! Adding no:label will show everything without a label.