Skip to content

Pull requests: leanprover/lean4

New pull request New
428 Open 9,054 Closed
428 Open 9,054 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: remove outdated trust0 test toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12401 opened Feb 9, 2026 by Garmelon Loading…
2
doc: the different chunks of the pass manager 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
#12400 opened Feb 9, 2026 by hargoniX Loading…
2
fix: force unfolding of the Decidable instace in Decidable.rec changelog-tactics User facing tactics
#12399 opened Feb 9, 2026 by wkrozowski • Draft
1
experiment: never inline f._redArg into f 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
#12396 opened Feb 9, 2026 by Kha • Draft
5
feat: pick up specs from the local context in mvcgen changelog-language Language features and metaprograms
#12395 opened Feb 9, 2026 by sgraf812 Loading…
feat: add pretty printer flag to instantiate non-ground delayed assignments changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12393 opened Feb 9, 2026 by sgraf812 Loading…
chore: be consistent about setting [inline] before compilation 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
#12389 opened Feb 9, 2026 by Kha Loading…
6
fix: avoid destroying reuse potential in LCNF simp toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12388 opened Feb 9, 2026 by hargoniX • Draft
10
feat: Array.mergeSort 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
#12385 opened Feb 9, 2026 by datokrat • Draft
4
refactor: port IR.SimpCase to LCNF changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12384 opened Feb 9, 2026 by hargoniX Loading…
13
feat: object graph dump toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12383 opened Feb 9, 2026 by hargoniX • Draft
feat: extend +locals to include import all'd definitions changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12382 opened Feb 9, 2026 by kim-em • Draft
2
fix: binderNameHint with simp changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12380 opened Feb 8, 2026 by Rob23oba Loading…
8
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 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
#12352 opened Feb 6, 2026 by datokrat • Draft
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 changelog-language Language features and metaprograms 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 Loading…
3
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
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
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
ProTip! no:milestone will show everything without a milestone.