Skip to content

Pull requests: leanprover/lean4

New pull request New
393 Open 8,682 Closed
393 Open 8,682 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: don't extend Applicative in Alternative 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
#11925 opened Jan 7, 2026 by JovanGerb Loading…
3
feat: add typeclass instances for common types toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11924 opened Jan 7, 2026 by alok • Draft
2 tasks done
2
feat: add lake shake command changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11921 opened Jan 7, 2026 by kim-em Loading…
7
fix: improve error message for initialize with missing Nonempty instance changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11919 opened Jan 6, 2026 by kim-em Loading…
2
feat: filter out deprecated lemmas from suggestions in exact?/rw? changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11918 opened Jan 6, 2026 by kim-em Loading…
2
feat: add a symbol gadget for non linear Array copies changelog-compiler Compiler, runtime, and FFI 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
#11916 opened Jan 6, 2026 by hargoniX Loading…
3
perf: fix two non linearities in the language server toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11915 opened Jan 6, 2026 by hargoniX Loading…
4
feat: grind annotations in Init.Data.Nat.Div.Basic builds-manual CI has verified that the Lean Language Reference 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
#11913 opened Jan 6, 2026 by pirapira Loading…
2
doc: add missing docstrings to iterator library 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-doc Documentation 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
#11912 opened Jan 6, 2026 by david-christiansen Loading…
6
feat: Decidable instance for Nat.isPowerOfTwo changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11905 opened Jan 5, 2026 by georgerennie Loading…
3
fix: warn when Where is used instead of where in declarations changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11904 opened Jan 5, 2026 by kim-em Loading…
1
5
fix: avoid panic in async elaboration for theorems with docstrings in where changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#11896 opened Jan 4, 2026 by kim-em Loading…
1
3
refactor: change definition of closed terms
#11891 opened Jan 4, 2026 by hargoniX • Draft
12
feat: re-integrate lean4checker as leanchecker 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 changelog-other 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
#11887 opened Jan 3, 2026 by Kha • Draft
2 tasks done
2
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. builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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 Loading…
26
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…
3
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…
4
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…
3
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
ProTip! Updated in the last three days: updated:>2026-01-04.