Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,147 Open 38,968 Closed
3,147 Open 38,968 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

chore(CategoryTheory/Comma): more implicit_reducible definitions t-category-theory Category theory
#42762 opened Aug 14, 2026 by joelriou Contributor Loading…
1
feat(CategoryTheory/Presentable): lemmas about sharply smaller regular cardinals t-category-theory Category theory t-set-theory Set theory
#42761 opened Aug 14, 2026 by joelriou Contributor Loading…
1
feat(Analysis/SpecialFunction): bessel function of the first kind t-analysis Analysis (normed *, calculus)
#42760 opened Aug 14, 2026 by wwylele Collaborator Loading…
@mcdoll
4
feat(CategoryTheory/Subobject): extend image subobject API blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#42759 opened Aug 14, 2026 by mckoen Collaborator Loading…
1 task
2
feat(ModelTheory): add syntax and semantics for infinitary logic LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-logic Logic (model theory, etc)
#42758 opened Aug 14, 2026 by cameronfreer Contributor Loading…
3
feat(CategoryTheory/Subobject): extend exists and pullback API t-category-theory Category theory
#42757 opened Aug 14, 2026 by mckoen Collaborator Loading…
1
chore: get cache large-import Automatically added label for PRs with a significant increase in transitive imports
#42756 opened Aug 14, 2026 by thorimur Contributor • Draft
1
chore: use private proof elaborator to remove set_option backward.privateInPublic
#42755 opened Aug 14, 2026 by thorimur Contributor • Draft
1
feat(GroupTheory/SpecificGroups/Cyclic): comparison and index of subgroups generated by powers t-group-theory Group theory
#42754 opened Aug 14, 2026 by xroblot Collaborator Loading…
3
refactor: redefine spectralRadius in terms of quasispectrum merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-analysis Analysis (normed *, calculus)
#42753 opened Aug 13, 2026 by j-loreaux Contributor Loading…
1
fix(Cache): give each cache process its own temporary file names CI Modifies the continuous integration setup or other automation
#42752 opened Aug 13, 2026 by kim-em Contributor Loading…
@bryangingechen
1
chore(Algebra/QuadraticAlgebra): rename map/mapEquiv to changeGenerator t-algebra Algebra (groups, rings, fields, etc)
#42751 opened Aug 13, 2026 by xroblot Collaborator Loading…
1
feat(Topology): generalise IsometricSmul to WeakPseudoEMetricSpace and friends blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) LLM-generated PRs with substantial input from LLMs - review accordingly
#42750 opened Aug 13, 2026 by felixpernegger Contributor Loading…
1 task
5
feat(RingTheory/Bialgebra): expose (Add)MonoidAlgebra.liftMulEquiv t-ring-theory Ring theory
#42749 opened Aug 13, 2026 by kim-em Contributor Loading…
1
chore(LinearAlgebra): tidy markdown headers t-algebra Algebra (groups, rings, fields, etc)
#42748 opened Aug 13, 2026 by harahu Contributor Loading…
1
feat(Topology): generalise Dilation to WeakPseudoEMetricSpace and friends blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) LLM-generated PRs with substantial input from LLMs - review accordingly
#42747 opened Aug 13, 2026 by felixpernegger Contributor Loading…
1 task
4
chore: remove outdated adaptation notes after #42161 t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42745 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
feat(Analysis/InnerProductSpace): complexification of Hilbert spaces t-analysis Analysis (normed *, calculus) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42744 opened Aug 13, 2026 by themathqueen Collaborator • Draft
1
chore(Tactic): mark two runtime-only imports as shake: keep delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). LLM-generated PRs with substantial input from LLMs - review accordingly t-meta Tactics, attributes or user commands
#42743 opened Aug 13, 2026 by bryangingechen Contributor Loading…
7
feat: the set of Fredholm operators between two Banach spaces is open blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-topology Topological spaces, uniform spaces, metric spaces, filters
#42742 opened Aug 13, 2026 by ADedecker Member Loading…
1 task
2
feat(Topology): generalise Isometry to WeakPseudoEMetricSpace and friends LLM-generated PRs with substantial input from LLMs - review accordingly t-topology Topological spaces, uniform spaces, metric spaces, filters
#42741 opened Aug 13, 2026 by felixpernegger Contributor Loading…
1 task
3
chore: mark AlgebraicGeometry.PrimeSpectrum.Top as implicit_reducible t-algebraic-geometry Algebraic geometry tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42740 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
chore(Order/Interval): define Unique (Iic 0) directly, drop a defeq option in Traj tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42739 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
1
chore(Data/Finset): mark Equiv.restrictPreimageFinset implicit_reducible t-measure-probability Measure theory / Probability theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42738 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
@EtienneC30
1
feat(Algebra/Order/Kleene): add Kleene algebra instances for MulOppos… 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)
#42737 opened Aug 13, 2026 by Jack1320 Loading…
2
ProTip! no:milestone will show everything without a milestone.