Skip to content

Pull requests: leanprover/lean4

New pull request New
660 Open 11,227 Closed
660 Open 11,227 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

perf: keep dependent tasks on a warm worker in the task manager changelog-compiler Compiler, runtime, and FFI downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15258 opened Sep 21, 2026 by Kha Member • Draft
3
feat: proper Min and Max on floats changelog-library Library 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
#15257 opened Sep 21, 2026 by TwoFX Member Loading…
fix: preserve literal plus signs in HTTP query encoding toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15254 opened Sep 21, 2026 by SkanderBog • Draft
1
feat: better assignment of synthOpaque mvars toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15253 opened Sep 21, 2026 by arthur-adjedj Contributor • Draft
fix: respect visibility for section variable autoParam helpers changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15249 opened Sep 21, 2026 by kim-em Collaborator Loading…
1
perf: wake only the waiters of a finished task in the task manager toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15248 opened Sep 21, 2026 by Kha Member • Draft
2
fix: track let-variables needed for value : type in Closure.mkValueTypeClosure changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15245 opened Sep 21, 2026 by kim-em Collaborator Loading…
1
2
fix: cbv on ite and dite with trivial conditions 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
#15244 opened Sep 20, 2026 by Rob23oba Contributor Loading…
1
perf: resolve boolean options once into a Core.Context flag word downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15243 opened Sep 20, 2026 by Kha Member Loading…
5
fix: preserve sticky counts in deletion cascades toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15241 opened Sep 20, 2026 by vincentqb Loading…
perf: reduce wake-ups and keep dependent tasks on a warm worker in the task manager changelog-compiler Compiler, runtime, and FFI downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15236 opened Sep 20, 2026 by Kha Member • Draft
4
feat: basic reverse iterators for Range, Array, Vector toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15233 opened Sep 20, 2026 by Bubbler-4 Loading…
perf: non-quadratic floatLetIn toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15229 opened Sep 19, 2026 by hargoniX Member Loading…
4
fix: warn on deprecated fields in structure instances toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15225 opened Sep 19, 2026 by skwh54 • Draft
1
vibe-ported intblasting tests toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15224 opened Sep 18, 2026 by andres-erbsen • Draft
feat: delay elab of full file toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15222 opened Sep 18, 2026 by AugustDeer • Draft
1
feat: better handling of one-field-structure constructors and projections in induction/cases changelog-language Language features and metaprograms downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15221 opened Sep 18, 2026 by datokrat Contributor • Draft
1
fix: prevent duplicate module initialization in C codegen 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
#15219 opened Sep 18, 2026 by iyassou • Draft
1
feat: extensible code formatter toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15218 opened Sep 18, 2026 by mhuisi Contributor • Draft
1
fix: reuse the instances of a non-exposed definition in inferInstanceAs changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15216 opened Sep 18, 2026 by gasparattila Loading…
1
1
fix: use pi_congr instead of forall_congr, deprecate the latter awaiting-review Waiting for someone to review the PR changelog-library Library downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15215 opened Sep 18, 2026 by sgraf812 Contributor Loading…
1
4
test: robin's Level.isEquiv downstream Request a downstream-lean4 adaptation PR. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15210 opened Sep 17, 2026 by arthur-adjedj Contributor • Draft
4
fix: include mutex in single-threaded thread.h awaiting-review Waiting for someone to review the PR changelog-compiler Compiler, runtime, and FFI
#15209 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: error instead of panic on excess syntax match patterns awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms
#15208 opened Sep 17, 2026 by Chessing234 Loading…
1
2
fix: preserve outer messages around #guard_msgs awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#15207 opened Sep 17, 2026 by Chessing234 Loading…
1
2
ProTip! Exclude everything labeled bug with -label:bug.