Skip to content

Pull requests: leanprover/lean4

New pull request New
422 Open 8,934 Closed
422 Open 8,934 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 Nat.ext_div_mod and Int.ext_ediv_emod changelog-library Library
#12258 opened Jan 31, 2026 by kim-em Loading…
try fix: Avoid deadlock by not throttling workers when the task manager i… 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
#12255 opened Jan 30, 2026 by marcelolynch • Draft
2
feat: add array lemmas about sum/min/max breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#12249 opened Jan 30, 2026 by datokrat • Draft
2
chore: delete dead C++ code 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
#12248 opened Jan 30, 2026 by Kha Loading…
2
feat: @[instance_reducible] breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#12247 opened Jan 30, 2026 by leodemoura • Draft
3
feat: do not simp instances changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12244 opened Jan 30, 2026 by leodemoura Loading…
2
fix: more floatLetIn nonlinearity 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
#12241 opened Jan 29, 2026 by Rob23oba • Draft
6
feat: allow for extensibility of the main step in Sym.Simp changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12237 opened Jan 29, 2026 by wkrozowski Loading…
4
feat: add orElse combinator to Sym.Simp.Simproc changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12236 opened Jan 29, 2026 by wkrozowski Loading…
2
feat: simplify iterator step unfolding changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12234 opened Jan 29, 2026 by datokrat • Draft
2
perf: a non-updating single-subst instantiateMVar 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
#12233 opened Jan 29, 2026 by nomeata • Draft
4
feat: grindify take_drop and drop_drop 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
#12232 opened Jan 29, 2026 by datokrat • Draft
4
WIP: refactoring towards verified String.split 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 WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet.
#12228 opened Jan 29, 2026 by TwoFX • Draft
6
fix: handle universe polymorphism in ground grind theorems changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12226 opened Jan 29, 2026 by kim-em Loading…
3
perf: normalize levels after instantiateMVars breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#12225 opened Jan 29, 2026 by JovanGerb • Draft
4
fix: IO.Process.spawn empty env var 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
#12220 opened Jan 28, 2026 by tydeu Loading…
2
fix: unification issue in proofs generated by Lean.Meta.MkIffOfInductiveProp changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12219 opened Jan 28, 2026 by wkrozowski Loading…
1
2
feat: one axiom per native computation 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
#12217 opened Jan 28, 2026 by nomeata Loading…
1
9
feat: Std.Iter.isEmpty 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
#12212 opened Jan 28, 2026 by datokrat • Draft
2
feat: print backtrace on stack overflow 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 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12208 opened Jan 28, 2026 by Kha • Draft
2
WIP perf: what happens if we ignore instances in expressions in tabled typeclass resolution? 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
#12206 opened Jan 28, 2026 by Vierkantor • Draft
4
feat: lake: hard link restored artifacts 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-lake Lake 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
#12203 opened Jan 28, 2026 by tydeu • Draft
2
feat: backward.isDefEq.respectTransparency changelog-language Language features and metaprograms
#12179 opened Jan 27, 2026 by leodemoura • Draft
fix: remove unnecessary dependency of pairwise_iff_getElem and add nodup_iff_getElem_inj toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12166 opened Jan 26, 2026 by linesthatinterlace Loading…
4
feat: introduce HTTP/1.1 server changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12151 opened Jan 25, 2026 by algebraic-dev Loading…
@algebraic-dev
3
ProTip! Updated in the last three days: updated:>2026-01-27.