Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,988 Open 31,272 Closed
1,988 Open 31,272 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(NumberTheory): add unitary divisor sum function new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#33838 opened Jan 11, 2026 by chainstart Loading…
5 of 6 tasks
1
feat: Tendsto (√·) atTop atTop t-data Data (lists, quotients, numbers, etc) t-order Order theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#33837 opened Jan 11, 2026 by Komyyy Loading…
1
feat: add lemma le_abs_of_dvd easy < 20s of review time. See the lifecycle page for guidelines. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
#33836 opened Jan 11, 2026 by VagelisKitsios Loading…
1
chore(Computability/Primrec): split file t-computability Computability theory (TMs, DFAs, languages, grammars, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#33835 opened Jan 11, 2026 by BoltonBailey Loading…
3
feat(CategoryTheory/NatTrans): use to_dual blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33834 opened Jan 11, 2026 by JovanGerb Loading…
2 tasks
3
feat(reassoc): tag the generated declaration with to_dual none t-meta Tactics, attributes or user commands
#33833 opened Jan 11, 2026 by JovanGerb Loading…
1
feat(Algebra): localization preserves unique factorization t-algebra Algebra (groups, rings, fields, etc)
#33832 opened Jan 11, 2026 by alreadydone Loading…
1
refactor(RingTheory/Polynomial/SmallDegreeVieta): convert to {p : R[X]} (hp : p.natDegree = 2) t-ring-theory Ring theory
#33831 opened Jan 11, 2026 by vihdzp Loading…
1
feat(Manifold/MFDeriv): MDifferentiable.pow and variants t-differential-geometry Manifolds etc
#33830 opened Jan 11, 2026 by seewoo5 Loading…
1
chore(Algebra/Group/Center): golf some stuff t-algebra Algebra (groups, rings, fields, etc)
#33828 opened Jan 10, 2026 by themathqueen Loading…
8
fix: restore #lint via Mathlib.Init easy < 20s of review time. See the lifecycle page for guidelines. large-import Automatically added label for PRs with a significant increase in transitive imports t-linter Linter
#33827 opened Jan 10, 2026 by thorimur Loading…
1
chore: golf using grind
#33826 opened Jan 10, 2026 by euprunin Loading…
1
chore: golf using grind
#33825 opened Jan 10, 2026 by euprunin Loading…
1
doc: update the doc of Bolzano-Weierstrass documentation Improvements or additions to documentation t-topology Topological spaces, uniform spaces, metric spaces, filters
#33824 opened Jan 10, 2026 by Komyyy Loading…
2
chore(GroupTheory/GroupAction/Defs): golf orbitRel.iseqv t-group-theory Group theory
#33823 opened Jan 10, 2026 by SnirBroshi Loading…
1
feat(Meta/CategoryTheory): cancelIso simproc blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory t-meta Tactics, attributes or user commands
#33822 opened Jan 10, 2026 by robin-carlier Loading…
1 task
20
feat(LinearAlgebra/Matrix/Hermitian): add IsSkewHermitian predicate t-algebra Algebra (groups, rings, fields, etc)
#33821 opened Jan 10, 2026 by JohnnyTeutonic Loading…
3
feat(CategoryTheory): use push attribute for CategoryTheory.inv. t-category-theory Category theory
#33820 opened Jan 10, 2026 by robin-carlier Loading…
3
feat(Analysis/Convex): diameter of a standard simplex t-analysis Analysis (normed *, calculus)
#33819 opened Jan 10, 2026 by bjornsolheim Loading…
5
feat(Algebra/Lie/Classical): finrank of sl(n) equals n² - 1 t-algebra Algebra (groups, rings, fields, etc)
#33818 opened Jan 10, 2026 by JohnnyTeutonic Loading…
8
fix(Combinatorics/Enumerative/Schroder.lean): Fix the definition and theorem of smallSchroder. large-import Automatically added label for PRs with a significant increase in transitive imports new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#33817 opened Jan 10, 2026 by FlAmmmmING Loading…
1
fix: whitespace around conditional variance t-measure-probability Measure theory / Probability theory
#33815 opened Jan 10, 2026 by grunweg Loading…
1
feat(Manifold/MFDeriv): add MDifferentiable.pow with FunProp blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-differential-geometry Manifolds etc
#33814 opened Jan 10, 2026 by seewoo5 Loading…
1 task
2
feat: define List.offDiag t-data Data (lists, quotients, numbers, etc)
#33812 opened Jan 10, 2026 by urkud Loading…
3
feat: add instances of LawfulInv blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) WIP Work in progress
#33810 opened Jan 9, 2026 by dupuisf Loading…
1 task
2
ProTip! Updated in the last three days: updated:>2026-01-07.