Skip to content

Pull requests: leanprover/lean4

New pull request New
424 Open 8,990 Closed
424 Open 8,990 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

fix: docstring code suggestions take shadowing into account changelog-no Do not include this PR in the release changelog
#12321 opened Feb 5, 2026 by david-christiansen Loading…
2
fix: avoid unaligned pointer dereference 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
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
refactor: reset reuse pass to LCNF 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
#12315 opened Feb 4, 2026 by hargoniX • Draft
11
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
chore: CI: avoid fetching full repo in PR Release toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12309 opened Feb 4, 2026 by Kha Loading…
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 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
chore: do not rely on Name.lt for ordering fvars in acLt fast-ci Forces the use of large runners so that e.g. PR releases are created faster toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12306 opened Feb 4, 2026 by Kha • Draft
1
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
feat: lake: disabling the artifact cache also disables fetching changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12300 opened Feb 4, 2026 by tydeu • Draft
[draft] feat: add cbv_eval attribute changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12296 opened Feb 3, 2026 by wkrozowski • Draft
fix: type class resolution cache changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12286 opened Feb 3, 2026 by leodemoura Loading…
14
perf: improve over-applied cases in ToLCNF 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
#12284 opened Feb 2, 2026 by Rob23oba Loading…
5
fix: IO.FS.removeFile should delete read-only files 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
#12282 opened Feb 2, 2026 by tydeu Loading…
3
feat: define Squash as a Quotient 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
#12281 opened Feb 2, 2026 by vihdzp Loading…
4
feat: IO.FS.Metadata.numLinks 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
#12277 opened Feb 2, 2026 by tydeu Loading…
2
doc: improve comments around asyncMayModify 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
#12270 opened Feb 2, 2026 by Kha Loading…
2
chore: CI: bump dawidd6/action-download-artifact from 11 to 14 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12267 opened Feb 1, 2026 by dependabot bot Loading…
2
chore: CI: bump actions/upload-artifact from 5 to 6 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12266 opened Feb 1, 2026 by dependabot bot Loading…
2
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
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
8
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
ProTip! Add no:assignee to see everything that’s not assigned.