Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,077 Open 31,735 Closed
2,077 Open 31,735 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(Geometry/Polygons): define polygons, Euclidean polygons, and triangles Mathlib/Geometry/Polygons new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34392 opened Jan 25, 2026 by A-M-Berns Loading…
2 tasks done
1
chore(Logic): generalise universes for relator and relation t-logic Logic (model theory, etc)
#34391 opened Jan 25, 2026 by b-mehta • Draft
1
feat(Real): add bound y * exp(-y) ≤ exp(-1) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34390 opened Jan 25, 2026 by jackabatc Loading…
2
chore(Analysis/Asymptotics): remove unnecessary hypothesis from isEquivalent_of_tendsto_one t-analysis Analysis (normed *, calculus)
#34389 opened Jan 24, 2026 by vasnesterov Loading…
1
feat(Order/Minimal): Minimal is equivalent to IsLeast if LE is total t-order Order theory
#34388 opened Jan 24, 2026 by Jun2M Loading…
2
chore: don't expose Shrink t-logic Logic (model theory, etc)
#34387 opened Jan 24, 2026 by plp127 Loading…
3
chore(Order/RelClasses): resolve TODO t-order Order theory
#34386 opened Jan 24, 2026 by plp127 Loading…
4
chore: add deprecation for Cardinal.nat_lt_aleph0 delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-set-theory Set theory
#34385 opened Jan 24, 2026 by Ruben-VandeVelde Loading…
3
chore: deprecate memoFix and replaceRec delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-meta Tactics, attributes or user commands
#34384 opened Jan 24, 2026 by JovanGerb Loading…
5
feat(Geometry/Convex/Cone): monotonicity and map lemmas for min/max cone tensor products t-convex-geometry Affine geometry, cones, simplices
#34383 opened Jan 24, 2026 by bjornsolheim Loading…
1
feat(Logic/Relation): transitive closure of symmetric relation is symmetric easy < 20s of review time. See the lifecycle page for guidelines. t-logic Logic (model theory, etc)
#34382 opened Jan 24, 2026 by b-mehta Loading…
3
feat(Probability): Generalize some theorems by replacing StronglyAdapted with Adapted t-measure-probability Measure theory / Probability theory
#34381 opened Jan 24, 2026 by CoolRmal Loading…
1
feat(GroupTheory/Focal): add focal subgroup theorem new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-group-theory Group theory
#34380 opened Jan 24, 2026 by Rogerhu12 Loading…
1
refactor(EMetricSpace): rename EMetric.ball -> Metric.eball
#34379 opened Jan 24, 2026 by urkud Loading…
1
feat(Analysis/SpecialFunctions/Gamma/Deriv): add deriv_Gamma_add_one t-analysis Analysis (normed *, calculus)
#34378 opened Jan 24, 2026 by tb65536 Loading…
1
chore(GroupTheory/Congruence/Basic): remove redundant import all t-group-theory Group theory
#34377 opened Jan 24, 2026 by JovanGerb Loading…
1
feat(MeasureTheory/Function/AEEqOfLIntegral): introduce lemmas for rewriting a.e. inequalities easy < 20s of review time. See the lifecycle page for guidelines. 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
#34375 opened Jan 24, 2026 by jvanwinden Loading…
4
feat(MeasureTheory): characterise when a measure is supported on a finset t-measure-probability Measure theory / Probability theory
#34374 opened Jan 24, 2026 by YaelDillies Loading…
1
feat(CategoryTheory/Triangulated): a triangulated subcategory is a pretriangulated category 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-category-theory Category theory WIP Work in progress
#34373 opened Jan 24, 2026 by joelriou Loading…
2 tasks
2
feat(CategoryTheory/Shift): the shift on a full subcategory large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#34372 opened Jan 24, 2026 by joelriou Loading…
1
feat: module instance on ContMDiffMap t-differential-geometry Manifolds etc WIP Work in progress
#34371 opened Jan 24, 2026 by grunweg Loading…
2
feat: tangentMap(Within)_snd easy < 20s of review time. See the lifecycle page for guidelines. t-differential-geometry Manifolds etc
#34369 opened Jan 24, 2026 by grunweg Loading…
2
feat(CategoryTheory/Triangulated): bounded objects for a t-structure t-category-theory Category theory
#34368 opened Jan 24, 2026 by joelriou Loading…
1
feat(CategoryTheory/ObjectProperty): stability unfer finite products t-category-theory Category theory
#34366 opened Jan 24, 2026 by joelriou Loading…
1
feat(Chebyshev/RootsExtrema): bound iterated derivatives of Chebyshev T on [-1, 1]
#34364 opened Jan 24, 2026 by YuvalFilmus Loading…
1
ProTip! no:milestone will show everything without a milestone.