Skip to content

Pull requests: leanprover/lean4

New pull request New
426 Open 9,034 Closed
426 Open 9,034 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

chore: missing annotations changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12368 opened Feb 6, 2026 by leodemoura Loading…
2
feat: vector iterator 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
#12363 opened Feb 6, 2026 by datokrat • Draft
2
fix: handling of ite/dite expressions in cbv tactic changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12361 opened Feb 6, 2026 by wkrozowski • Draft
2
feat: verification of string patterns toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12360 opened Feb 6, 2026 by TwoFX • Draft
2
feat: prove xs.extract start stop = (xs.take stop).drop start for lists 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
#12359 opened Feb 6, 2026 by datokrat Loading…
3
chore: refactor let and match elaborator to be used from the do elaborator toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12354 opened Feb 6, 2026 by sgraf812 Loading…
4
feat: upstream slice API improvements from human-eval-lean toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12352 opened Feb 6, 2026 by datokrat • Draft
2
feat: shake: track [csimp] uses changelog-other toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12351 opened Feb 6, 2026 by Kha • Queued
2
feat: some unification hints 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-library Library fast-ci Forces the use of large runners so that e.g. PR releases are created faster 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
#12341 opened Feb 6, 2026 by leodemoura Loading…
3
fix: use target type's instances in delta deriving 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
#12339 opened Feb 6, 2026 by kim-em • Draft
2
fix: remove iff True from array lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12330 opened Feb 5, 2026 by jt0202 Loading…
3
feat: move instance-class check to declaration site 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 merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12325 opened Feb 5, 2026 by Kha • Draft
4
fix: avoid unaligned pointer dereference changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12318 opened Feb 5, 2026 by eric-wieser Loading…
1
10
feat: make try? find induction proofs for forall-quantified goals toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12316 opened Feb 4, 2026 by kim-em • Draft
feat: language server adaptions for multi-version workspaces toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12310 opened Feb 4, 2026 by mhuisi • Draft
chore: CI: avoid fetching full repo in PR Release toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12309 opened Feb 4, 2026 by Kha Loading…
feat: instances should always be non-recursive awaiting-mathlib We should not merge this until we have a successful Mathlib build fast-ci Forces the use of large runners so that e.g. PR releases are created faster mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12307 opened Feb 4, 2026 by Kha • Draft
2
chore: do not rely on Name.lt for ordering fvars in acLt builds-mathlib CI has verified that Mathlib builds against this PR fast-ci Forces the use of large runners so that e.g. PR releases are created faster 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
#12306 opened Feb 4, 2026 by Kha • Draft
2
refactor: eliminate simp +instances uses related to iterators/ranges/slices toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12304 opened Feb 4, 2026 by datokrat • Draft
3
perf: experiment: separate defeq/whnf kernel diagnostics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12303 opened Feb 4, 2026 by nomeata • Draft
5
feat: lake: disabling the artifact cache also disables fetching 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
#12300 opened Feb 4, 2026 by tydeu • Draft
1
feat: add cbv_eval attribute changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12296 opened Feb 3, 2026 by wkrozowski • Draft
15
fix: type class resolution cache changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12286 opened Feb 3, 2026 by leodemoura Loading…
14
fix: IO.FS.removeFile should delete read-only files on Windows 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 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
#12282 opened Feb 2, 2026 by tydeu Loading…
3
feat: define Squash as a Quotient 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
#12281 opened Feb 2, 2026 by vihdzp Loading…
4
ProTip! no:milestone will show everything without a milestone.