Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,692 Open 37,533 Closed
2,692 Open 37,533 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(scripts): update nolints.json auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done.
#40856 opened Jun 21, 2026 by mathlib-nolints Bot Loading…
2
feat(Data/ENNReal): add sum_div t-data Data (lists, quotients, numbers, etc)
#40855 opened Jun 20, 2026 by NoahW314 Contributor Loading…
1
chore(NumberTheory/PrimeCounting): minor golf 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)
#40854 opened Jun 20, 2026 by teorth Contributor Loading…
2
chore: fix bad indentation t-algebra Algebra (groups, rings, fields, etc)
#40853 opened Jun 20, 2026 by grunweg Contributor Loading…
1
feat: OddIndent linter t-linter Linter
#40852 opened Jun 20, 2026 by thorimur Contributor • Draft
1
feat(MeasureTheory/Integral/MeanInequalities): strict Hölder's inequality for Lebesgue integrals t-measure-probability Measure theory / Probability theory
#40851 opened Jun 20, 2026 by SnirBroshi Collaborator Loading…
1
chore: update Mathlib dependencies 2026-06-20 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#40849 opened Jun 20, 2026 by mathlib-update-dependencies Bot Loading…
1
WIP large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#40848 opened Jun 20, 2026 by fbarroero Collaborator Loading…
2
feat(Analysis/SpecialFunctions/Log/InvLog): add simp lemma form of deriv_inv_log new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#40847 opened Jun 20, 2026 by teorth Contributor Loading…
2
feat(Analysis/InnerProductSpace/TensorProduct): add TensorProduct.congrL 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 t-topology Topological spaces, uniform spaces, metric spaces, filters
#40846 opened Jun 20, 2026 by TJHeeringa Contributor Loading…
2 tasks
2
feat(FinitelyPresentedGroup): quotient of a finitely group by a subgroup which is finitely generated under normal closure is finitely presented new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory
#40845 opened Jun 20, 2026 by laredo02 Loading…
2
feat(Algebra/Divisibility/Basic): introduce right division (RightDvd) 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)
#40843 opened Jun 20, 2026 by ReemMelamed Loading…
2
feat(Topology/Algebra): add ContinuousLinearEquiv.ofContinuousLinearMap t-topology Topological spaces, uniform spaces, metric spaces, filters
#40841 opened Jun 20, 2026 by TJHeeringa Contributor Loading…
2
feat(MeasureTheory): use IsApply for Measure
#40840 opened Jun 20, 2026 by mcdoll Member • Draft
1
chore(RingTheory/Derivation/DifferentialRing): squeeze terminal simps awaiting-author A reviewer has asked the author a question or requested changes. t-ring-theory Ring theory
#40837 opened Jun 20, 2026 by yuanyi-350 Collaborator Loading…
@grunweg
3
feat(RingTheory/Ideal/Operations): pow_eq_bot t-ring-theory Ring theory
#40836 opened Jun 20, 2026 by fbarroero Collaborator Loading…
3
feat(Probability): add Paley-Zygmund inequality new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#40835 opened Jun 20, 2026 by Gracie-z Loading…
21
chore(Algebra/simp): remove @[simp] tag in AlgEquiv.coe_ringEquiv since it can be proven by simp easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#40834 opened Jun 20, 2026 by yuanyi-350 Collaborator Loading…
2
chore(MeasureTheory): remove redundant imports t-measure-probability Measure theory / Probability theory
#40832 opened Jun 20, 2026 by felixpernegger Contributor Loading…
4
Locally Free Sheaves on Affines t-algebraic-geometry Algebraic geometry WIP Work in progress
#40831 opened Jun 19, 2026 by Brian-Nugent Collaborator • Draft
1
feat(Analysis/Convex/Function): composition of strictly and non-strictly convex functions t-analysis Analysis (normed *, calculus)
#40830 opened Jun 19, 2026 by SnirBroshi Collaborator Loading…
1
feat(MeasureTheory): eLpNorm bound for a convex combination of functions brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#40829 opened Jun 19, 2026 by FrankieNC Collaborator Loading…
1
feat(MeasureTheory): coercion of a finite sum of scalar multiples in Lp brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory
#40827 opened Jun 19, 2026 by FrankieNC Collaborator Loading…
3
feat(ci): autolabel PRs with "Generated with Claude Code" CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly
#40826 opened Jun 19, 2026 by felixpernegger Contributor Loading…
4
feat(Analysis/FunctionalSpaces): the one-dimensional Poincaré inequality 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-measure-probability Measure theory / Probability theory
#40824 opened Jun 19, 2026 by alejandro-soto-franco Contributor Loading…
6
ProTip! Exclude everything labeled bug with -label:bug.