Skip to content

Pull requests: leanprover/lean4

New pull request New
386 Open 8,658 Closed
386 Open 8,658 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

refactor: change definition of closed terms
#11891 opened Jan 4, 2026 by hargoniX • Draft
6
feat: re-integrate lean4checker as leanchecker changelog-other
#11887 opened Jan 3, 2026 by Kha • Draft
2 tasks
fix: avoid panic in TagDeclarationExtension.tag on partial elaboration changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11882 opened Jan 3, 2026 by kim-em Loading…
2
fix: grind propagates 0 * a = 0 for CommSemiring changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11881 opened Jan 3, 2026 by kim-em Loading…
3
fix: show builtin syntax kind docs for antiquotation kinds
#11876 opened Jan 2, 2026 by alok • Draft
feat: unbox inductives in the compiler breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. 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
#11873 opened Jan 2, 2026 by Rob23oba • Draft
19
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: 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
ProTip! Updated in the last three days: updated:>2026-01-01.