Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,397 Open 35,285 Closed
2,397 Open 35,285 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(Algebra/Group/Submonoid/Defs): add OneMemClass.coe_nonempty easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#38288 opened Apr 20, 2026 by b-mehta Contributor Loading…
1
feat(Data/Set/Function): make mapsTo_univ a simp lemma easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#38287 opened Apr 20, 2026 by b-mehta Contributor Loading…
1
feat(Logic/Equiv/Defs): add coe_ofBijective simp lemma easy < 20s of review time. See the lifecycle page for guidelines. t-logic Logic (model theory, etc)
#38286 opened Apr 20, 2026 by b-mehta Contributor Loading…
1
feat(GroupTheory/GroupAction/FixedPoints): characterise when there are no fixed points by an action easy < 20s of review time. See the lifecycle page for guidelines. t-group-theory Group theory
#38285 opened Apr 20, 2026 by b-mehta Contributor Loading…
1
chore: remove shortcut instance that is no longer needed t-analysis Analysis (normed *, calculus)
#38284 opened Apr 20, 2026 by jcommelin Member Loading…
3
feat(Data/Finset/Image): add lemmas linking Finset.image with MapsTo/SurjOn/InjOn easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#38283 opened Apr 20, 2026 by b-mehta Contributor Loading…
1
chore(Algebra/Lie/Submodule): remove duplicate instance t-algebra Algebra (groups, rings, fields, etc)
#38282 opened Apr 20, 2026 by JovanGerb Contributor Loading…
1
chore(CategoryTheory): fix diamond for the preadditive structure on the opposite category t-category-theory Category theory
#38281 opened Apr 20, 2026 by joelriou Contributor Loading…
7
refactor(NumberTheory): golf Mathlib/NumberTheory/Cyclotomic/Basic codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38280 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
3
refactor(NumberTheory): golf Mathlib/NumberTheory/NumberField/Basic codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38279 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
2
refactor(NumberTheory): golf Mathlib/NumberTheory/ArithmeticFunction/Zeta codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38278 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
2
refactor(NumberTheory): golf Mathlib/NumberTheory/NumberField/Norm codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38277 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
2
feat(Data/Set/Function): add prod lemmas for InjOn, SurjOn, MapsTo, LeftInvOn t-data Data (lists, quotients, numbers, etc)
#38276 opened Apr 20, 2026 by b-mehta Contributor Loading…
1
feat: Add AffineEquiv.image_intrinsicInterior new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#38275 opened Apr 20, 2026 by TTony2019 Loading…
4
refactor(Analysis): golf Mathlib/Analysis/Complex/Trigonometric codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-analysis Analysis (normed *, calculus)
#38274 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
3
refactor(Analysis): golf Mathlib/Analysis/SpecialFunctions/Gamma/Basic codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-analysis Analysis (normed *, calculus)
#38273 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
2
refactor(Analysis): golf Mathlib/Analysis/Normed/Operator/Mul awaiting-author A reviewer has asked the author a question or requested changes. codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-analysis Analysis (normed *, calculus)
#38272 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
6
feat(Geometry/Manifold): The Tangent Functor on MfldCat blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-differential-geometry Manifolds etc
#38270 opened Apr 20, 2026 by Deicyde Contributor • Draft
1 task
3
feat(Combinatorics/Additive): link Freiman homs and Freiman isos tighter
#38269 opened Apr 20, 2026 by b-mehta Contributor • Draft
1
feat(ProbabilityTheory): add APIs for predicationPart and martingalePart brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#38267 opened Apr 20, 2026 by CoolRmal Contributor Loading…
1
feat(Order/CompleteLatticeIntervals): ConditionallyCompleteLinearOrderBot for Set.Iio t-order Order theory
#38266 opened Apr 20, 2026 by staroperator Collaborator Loading…
3
feat(CategoryTheory): add MorphismProperty.paths awaiting-author A reviewer has asked the author a question or requested changes. t-category-theory Category theory
#38264 opened Apr 19, 2026 by peabrainiac Collaborator Loading…
2
chore: fix implicit-reducible diamond in Lie subalgebras t-algebra Algebra (groups, rings, fields, etc)
#38260 opened Apr 19, 2026 by sgouezel Contributor Loading…
8
feat(CategoryTheory): MorphismProperty.single t-category-theory Category theory
#38257 opened Apr 19, 2026 by joelriou Contributor Loading…
1
chore: fix implicit-reducible diamond in languages t-logic Logic (model theory, etc)
#38256 opened Apr 19, 2026 by sgouezel Contributor Loading…
1
ProTip! Adding no:label will show everything without a label.