Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,150 Open 39,057 Closed
3,150 Open 39,057 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(FieldTheory/IntermediateField/Adjoin): fix recursors t-algebra Algebra (groups, rings, fields, etc)
#42856 opened Aug 17, 2026 by plp127 Contributor Loading…
1
feat(RingTheory/MvPolynomial/MonomialOrder): add primed versions of lemmas t-ring-theory Ring theory
#42855 opened Aug 17, 2026 by NoahW314 Contributor Loading…
1
chore: update Mathlib dependencies 2026-08-17 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#42854 opened Aug 17, 2026 by mathlib-update-dependencies Bot Loading…
1
chore(RingTheory/MvPolynomial/MonomialOrder): rename degree_subsingleton to degree_of_subsingleton t-ring-theory Ring theory
#42853 opened Aug 17, 2026 by NoahW314 Contributor Loading…
1
feat(Tactic) : inclusion tactic (highly extensible engine for interval arithmetic, ball arithmetic etc...)
#42850 opened Aug 17, 2026 by DavidLedvinka Collaborator • Draft
1
feat(Analysis/LocallyConvex): induction principles for WithSeminorm t-analysis Analysis (normed *, calculus)
#42849 opened Aug 17, 2026 by mcdoll Member Loading…
1
chore(Analysis/LocallyConvex): add missing lemmas and rename t-analysis Analysis (normed *, calculus)
#42848 opened Aug 17, 2026 by mcdoll Member Loading…
1
feat(Geometry/Manifold): pull back charted space and groupoid structures along a homeomorphism new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-differential-geometry Manifolds etc
#42847 opened Aug 17, 2026 by Rshin2024 Loading…
2
feat(Analysis/Convex): egauge of a seminorm balls t-analysis Analysis (normed *, calculus)
#42846 opened Aug 17, 2026 by mcdoll Member Loading…
1
feat(Order/Monoid/Unbundled/Basic): left multiplication is strictly monotone if and only if it is monotone and left-cancellative t-algebra Algebra (groups, rings, fields, etc)
#42845 opened Aug 16, 2026 by homeowmorphism Contributor Loading…
2
refactor(Logic/Hydra): cleanup file t-logic Logic (model theory, etc)
#42844 opened Aug 16, 2026 by plp127 Contributor Loading…
1
feat(Combinatorics/SimpleGraph): transition matrix of the simple random walk 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-combinatorics Combinatorics
#42843 opened Aug 16, 2026 by than4213 Contributor Loading…
4
chore(CategoryTheory/Limits/Shapes/Terminal): use to_dual t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42842 opened Aug 16, 2026 by JovanGerb Contributor Loading…
1
feat: a bounded variation function is continuous off a countable set t-topology Topological spaces, uniform spaces, metric spaces, filters
#42841 opened Aug 16, 2026 by sgouezel Contributor Loading…
1
feat(Combinatorics/SimpleGraph/Connectivity): simple graph is 2-edge-connected iff it has no bridge new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#42839 opened Aug 16, 2026 by JadAbouHawili Contributor Loading…
3
feat(Order/SupClosed): a lower directed set is sup-closed easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#42838 opened Aug 16, 2026 by SnirBroshi Collaborator Loading…
1
feat(Order/Directed): the empty set is directed easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#42837 opened Aug 16, 2026 by SnirBroshi Collaborator Loading…
1
feat(NumberTheory/Padics): the Amice transform is a ring isomorphism blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#42836 opened Aug 16, 2026 by loefflerd Contributor Loading…
2 tasks
2
feat(RingTheory/NoetherNormalization): add that s is Krull dimension to theorem statements blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) 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-ring-theory Ring theory
#42835 opened Aug 16, 2026 by rshlyakh Contributor Loading…
1 task
4
doc(Data/Rel): fix variable name in Relation.Map example new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
#42834 opened Aug 16, 2026 by ashebson Loading…
2
feat(Combinatorics/SimpleGraph/Connnectivity): efficient decidability instances LLM-generated PRs with substantial input from LLMs - review accordingly t-combinatorics Combinatorics
#42833 opened Aug 16, 2026 by YaelDillies Contributor Loading…
1
feat(NumberTheory/Padics): the Amice transform t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#42832 opened Aug 16, 2026 by loefflerd Contributor Loading…
2
feat(CategoryTheory/Linear): category algebra of R-linear category awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-category-theory Category theory
#42831 opened Aug 16, 2026 by ray-shang Loading…
5
refactor: change ProbabilityMeasure.map to not require measurability t-measure-probability Measure theory / Probability theory
#42830 opened Aug 16, 2026 by EtienneC30 Member • Draft
2
feat(Topology/InfiniteSum): applying a tsum of CLM with operator norm t-topology Topological spaces, uniform spaces, metric spaces, filters
#42829 opened Aug 16, 2026 by wwylele Collaborator Loading…
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.