Skip to content

Pull requests: leanprover/lean4

New pull request New
458 Open 9,579 Closed
458 Open 9,579 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: symm tactic should synthesize instances changelog-language Language features and metaprograms
#13047 opened Mar 23, 2026 by kmill Loading…
1
feat: add permutation theorem support to Sym.simp changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13046 opened Mar 22, 2026 by leodemoura • Queued
2
fix: use commondir to resolve git directory in worktrees 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
#13045 opened Mar 22, 2026 by kim-em Loading…
2
[Backport releases/v4.29.0] fix: mark auxiliary definitions from normalizeInstance as meta
#13044 opened Mar 22, 2026 by github-actions bot Loading…
perf: use a cache in hasAssignableMVar 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
#13036 opened Mar 22, 2026 by JovanGerb Loading…
9
feat: pretty print level metavariables using index breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13030 opened Mar 22, 2026 by kmill Loading…
7
fix: lake: error on executables with duplicate root module names 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
#13028 opened Mar 21, 2026 by tydeu • Draft
1
4
fix: improved dependency tracking in metacontext and abstractMVars changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13025 opened Mar 21, 2026 by kmill • Draft
2
6
experiment: store environment extension changes in sparse map 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
#13020 opened Mar 21, 2026 by Kha • Draft
4
feat: add deprecated_arg attribute changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13011 opened Mar 20, 2026 by wkrozowski • Draft
4
experiment: use PersistentArray for Environment.extensions 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
#13010 opened Mar 20, 2026 by Kha • Draft
6
chore: update stage0 (evil version) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13009 opened Mar 20, 2026 by Rob23oba • Draft
2
doc: mark instantiateMVars docstring as such 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
#13006 opened Mar 20, 2026 by joneugster Loading…
1
1
feat: add deprecated_module changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13002 opened Mar 20, 2026 by wkrozowski • Draft
4
feat: String.simpEq simproc 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
#12995 opened Mar 19, 2026 by Rob23oba • Draft
3
fix: correctly set initHeartbeats in Lean.Environment.unsafeRunMetaM changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12994 opened Mar 19, 2026 by eric-wieser Loading…
7
feat: name the functional argument to brecOn in structural recursion 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
#12987 opened Mar 19, 2026 by nomeata Loading…
15
feat: List lemmas for tail/dropLast almost commuting with take/drop toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12976 opened Mar 19, 2026 by SnirBroshi Loading…
1
2
feat: theorems are opaque 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
#12973 opened Mar 18, 2026 by nomeata Loading…
1
10
feat: New foundations for mvcgen tactic
#12965 opened Mar 18, 2026 by volodeyka Loading…
feat: TR35 compatible format toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12958 opened Mar 18, 2026 by algebraic-dev • Draft
2
chore: check for empty PRs in CI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12956 opened Mar 17, 2026 by kim-em Loading…
2
demo
#12951 opened Mar 17, 2026 by datokrat • Draft
fix: record tasks from Command.logSnapshotTasks in snapshot tree 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
#12946 opened Mar 17, 2026 by Kha • Draft
5
perf: mark ReaderT context argument as borrow changelog-compiler Compiler, runtime, and FFI changes-stage0 Contains stage0 changes, merge manually using rebase fast-ci Forces the use of large runners so that e.g. PR releases are created faster 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
#12942 opened Mar 17, 2026 by hargoniX Loading…
6
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.