Skip to content

Pull requests: leanprover/lean4

New pull request New
526 Open 9,906 Closed
526 Open 9,906 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: add ToJson/FromJson for Unit changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13525 opened Apr 24, 2026 by Vtec234 Member Loading…
3
test: copy srcHash test data to temp dir before modifying lake-ci Run all Lake tests toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13524 opened Apr 24, 2026 by Kha Member Loading…
2
feat: add [no_fallback] attribute for tactic elaborators and macros changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13523 opened Apr 24, 2026 by Kha Member Loading…
2
fix: olean parts might not be in address order changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13522 opened Apr 24, 2026 by eric-wieser Contributor Loading…
3
fix: prevent undefined behavior without LEAN_MMAP changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13521 opened Apr 24, 2026 by eric-wieser Contributor Loading…
3
perf: lake: use List for BuildTrace.inputs 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
#13519 opened Apr 23, 2026 by tydeu Member • Draft
4
feat: lake: add support for running text linters from lake lint changelog-lake Lake lake-ci Run all Lake tests toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13513 opened Apr 23, 2026 by wkrozowski Contributor Loading…
11
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 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
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 breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
4
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 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 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
ProTip! Add no:assignee to see everything that’s not assigned.