Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,684 Open 37,524 Closed
2,684 Open 37,524 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(Integral/Layercake): fix latex in the module header easy < 20s of review time. See the lifecycle page for guidelines. t-measure-probability Measure theory / Probability theory
#40839 opened Jun 20, 2026 by lua-vr Contributor Loading…
2
chore(RingTheory/Spectrum/Prime/FreeLocus): squeeze terminal simps t-ring-theory Ring theory
#40838 opened Jun 20, 2026 by yuanyi-350 Collaborator Loading…
2
chore(RingTheory/Derivation/DifferentialRing): squeeze terminal simps t-ring-theory Ring theory
#40837 opened Jun 20, 2026 by yuanyi-350 Collaborator Loading…
3
feat(RingTheory/Ideal/Operations): pow_eq_bot t-ring-theory Ring theory
#40836 opened Jun 20, 2026 by fbarroero Collaborator Loading…
1
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…
12
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…
5
refactor(FieldTheory/Galois/IsGaloisGroup): generalize mulEquivAlgEquiv to domains t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#40822 opened Jun 19, 2026 by tb65536 Contributor Loading…
1 task done
2
chore: adaptations for batteries#1864 blocked-by-batt-PR This PR depends on a PR to Batteries
#40821 opened Jun 19, 2026 by grunweg Contributor Loading…
4 tasks
1
chore: adaptations for batteries#1863 blocked-by-batt-PR This PR depends on a PR to Batteries
#40820 opened Jun 19, 2026 by grunweg Contributor Loading…
1
chore(Combinatorics/SimpleGraph/Acyclic): golf IsAcyclic.path_unique easy < 20s of review time. See the lifecycle page for guidelines. t-combinatorics Combinatorics
#40818 opened Jun 19, 2026 by SnirBroshi Collaborator Loading…
1
fix(cache): carry cache misses across 'get' laters instead of using file existence as a proxy for 'done' CI Modifies the continuous integration setup or other automation
#40817 opened Jun 19, 2026 by marcelolynch Contributor Loading…
1
feat(Data/Nat/Factorial/Basic): add ascFactorial_le easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#40816 opened Jun 19, 2026 by NoahW314 Contributor Loading…
4
refactor(MeasureTheory/Measure/Typeclasses/NoAtoms): add deprecation for NoAtoms 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!
#40815 opened Jun 19, 2026 by ldiedering Contributor Loading…
1 task
3
feat(RingTheory/Ideal): prime avoidance for maximal ideal t-ring-theory Ring theory
#40814 opened Jun 19, 2026 by Thmoas-Guan Collaborator Loading…
1
feat(Algebra/Module): lemma for spanFinrank eq one t-algebra Algebra (groups, rings, fields, etc)
#40813 opened Jun 19, 2026 by Thmoas-Guan Collaborator Loading…
1
feat(RingTheory/HopfAlgebra): the antipode is the unique convolution … 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-ring-theory Ring theory
#40812 opened Jun 19, 2026 by karlesmarin Loading…
3
feat: linear map from L^p (mu) to L^p (nu) when nu is bounded by a multiple of mu t-measure-probability Measure theory / Probability theory
#40811 opened Jun 19, 2026 by sgouezel Contributor Loading…
2
refactor(MeasureTheory/Measure/Typeclasses/NoAtoms): rename NoAtoms to NullSingletonClass file-removed A Lean module was (re)moved without a `deprecated_module` annotation new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#40809 opened Jun 19, 2026 by ldiedering Contributor Loading…
3
ProTip! Mix and match filters to narrow down what you’re looking for.