Skip to content

Pull requests: leanprover/lean4

New pull request New
528 Open 9,891 Closed
528 Open 9,891 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

feat: user-specified init fn when loading plugins builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms lake-ci Run all Lake tests 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
#13510 opened Apr 22, 2026 by tydeu Member • Draft
2
feat: pluggable pure/bind builders for do elaboration changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13507 opened Apr 22, 2026 by sgraf812 Contributor Loading…
2
feat: inject unreachable! after break-less repeat changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13506 opened Apr 22, 2026 by sgraf812 Contributor Loading…
2
experiment: disable cse toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13505 opened Apr 22, 2026 by hargoniX Contributor • Draft
4
test: tests/lake/run_test.sh builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog lake-ci Run all Lake tests 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
#13501 opened Apr 22, 2026 by tydeu Member Loading…
5
feat: lake: empty build detection & --allow-empty builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake lake-ci Run all Lake tests 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
#13500 opened Apr 22, 2026 by tydeu Member Loading…
2
fix: handle interrupted reads 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
#13493 opened Apr 21, 2026 by eric-wieser Contributor Loading…
6
feat: add @[backward_defeq] attribute and local useBackward simp option builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms changelog-tactics User facing tactics 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
#13492 opened Apr 21, 2026 by nomeata Collaborator • Draft
2
feat: add Nat.powMod with GMP-backed extern for fast modular exponentiation changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13490 opened Apr 21, 2026 by kim-em Collaborator • Draft
8
fix: propagate parent cancel token to asTask subtasks via callbacks 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
#13488 opened Apr 20, 2026 by nomeata Collaborator • Draft
1
2
fix: statement of eqRec_heq_iff 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-no Do not include this PR in the release changelog 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
#13484 opened Apr 20, 2026 by Rob23oba Contributor Loading…
2
[Backport releases/v4.30.0] fix: wrapInstance: do not leak via un-reducible instances
#13481 opened Apr 20, 2026 by github-actions Bot Loading…
experiment: differential leanir benchmarking
#13478 opened Apr 19, 2026 by Kha Member • Draft
8
feat: add script/count-blocked-by-build-error builds-mathlib CI has verified that Mathlib 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
#13471 opened Apr 19, 2026 by kim-em Collaborator Loading…
2
refactor: lake: use InputVer in Dependency toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13470 opened Apr 19, 2026 by tydeu Member • Draft
2
feat: add tryRecv and hasPendingData to TCP to speed up recvSelector.tryFn changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13466 opened Apr 18, 2026 by algebraic-dev Member Loading…
@algebraic-dev
3
fix: avoid duplicate buffered writes when IO.Process.output exec fails changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13464 opened Apr 18, 2026 by kim-em Collaborator Loading…
1
2
feat: add List take/drop lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13462 opened Apr 18, 2026 by kim-em Collaborator • Draft
2
feat: add missing List foldl lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13460 opened Apr 18, 2026 by kim-em Collaborator • Draft
5
feat: add Array and Vector set! lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13459 opened Apr 18, 2026 by kim-em Collaborator • Draft
2
feat: add Nat.or_two_pow_eq_add_of_lt changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13458 opened Apr 18, 2026 by kim-em Collaborator Loading…
2
feat: add ByteArray indexing and set! lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13457 opened Apr 18, 2026 by kim-em Collaborator Loading…
2
feat: add lake build --summary flag changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13454 opened Apr 18, 2026 by kim-em Collaborator Loading…
1
4
feat: informative metavariable hovers, better delayed assignment pretty printing 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-pp Pretty printing 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
#13446 opened Apr 17, 2026 by kmill Collaborator Loading…
4
perf: json string parser fast path 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 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
#13443 opened Apr 17, 2026 by hargoniX Contributor • Draft
4
ProTip! Type g i on any issue or pull request to go back to the issue listing page.