Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,076 Open 39,493 Closed
3,076 Open 39,493 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

refactor(Combinatorics/Partition): eliminate T2Space requirement from generating function t-combinatorics Combinatorics
#43220 opened Aug 30, 2026 by wwylele Collaborator Loading…
3
feat(CategoryTheory/Action): an adjunction induces an adjunction on Action categories 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-category-theory Category theory
#43219 opened Aug 30, 2026 by landonfox00 • Draft
3
feat(Linter): port ERR_ARR style linter to Lean new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-linter Linter
#43217 opened Aug 29, 2026 by tanishjain758-prog Loading…
4
feat(Combinatorics/SimpleGraph/Clique): independence number is zero iff the graph has no vertices new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#43216 opened Aug 29, 2026 by JadAbouHawili Contributor Loading…
3
feat(Data/Nat/Nth): nth_add_one_le_iff t-data Data (lists, quotients, numbers, etc)
#43215 opened Aug 29, 2026 by teorth Contributor Loading…
1
feat(Analysis/Normed/Affine): mapping ball/sphere by homothety t-analysis Analysis (normed *, calculus)
#43214 opened Aug 29, 2026 by wwylele Collaborator Loading…
2
feat(Geometry/Manifold): smooth Urysohn on a finite-dim normed space t-differential-geometry Manifolds etc
#43213 opened Aug 29, 2026 by teorth Contributor Loading…
2
doc(Basic/IsEmpty/Basic): add module header easy < 20s of review time. See the lifecycle page for guidelines.
#43212 opened Aug 29, 2026 by harahu Contributor Loading…
2
feat(Geometry/Convex): ordered convex spaces LLM-generated PRs with substantial input from LLMs - review accordingly t-convex-geometry Affine geometry, cones, simplices
#43211 opened Aug 29, 2026 by YaelDillies Contributor Loading…
1
feat(Geometry): the standard simplex is path-connected 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-convex-geometry Affine geometry, cones, simplices
#43210 opened Aug 29, 2026 by joelriou Contributor Loading…
1 task
2
feat(Geometry/Convex): WithTop X is a convex space if X is LLM-generated PRs with substantial input from LLMs - review accordingly t-convex-geometry Affine geometry, cones, simplices
#43209 opened Aug 29, 2026 by YaelDillies Contributor Loading…
1
feat: definition + API for Cartan matrix realisations file-removed A Lean module was (re)moved without a `deprecated_module` annotation WIP Work in progress
#43208 opened Aug 29, 2026 by ocfnash Contributor Loading…
1
feat(NumberTheory/Harmonic): pointwise inv_riemannZeta_eq_sub_mul t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#43207 opened Aug 29, 2026 by teorth Contributor Loading…
@MichaelStollBayreuth
1
feat(Geometry): the barycenter of the standard simplex 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-convex-geometry Affine geometry, cones, simplices
#43206 opened Aug 29, 2026 by joelriou Contributor Loading…
1 task
2
feat(FieldTheory): extension is separable if its degree is less than the positive char t-algebra Algebra (groups, rings, fields, etc)
#43205 opened Aug 29, 2026 by wwylele Collaborator Loading…
3
chore(Basic/Logic/Basic): remove redundant grind pattern t-data Data (lists, quotients, numbers, etc)
#43204 opened Aug 29, 2026 by harahu Contributor Loading…
1
fix(Tactic/FastInstance): telescope over instance families t-meta Tactics, attributes or user commands
#43203 opened Aug 29, 2026 by SnirBroshi Collaborator Loading…
1
feat(Geometry): the standard simplex is compact large-import Automatically added label for PRs with a significant increase in transitive imports t-convex-geometry Affine geometry, cones, simplices
#43202 opened Aug 29, 2026 by joelriou Contributor Loading…
5
chore(Combinatorics/SimpleGraph): replace α,β,γ with V,W,X, etc t-combinatorics Combinatorics
#43201 opened Aug 29, 2026 by mitchell-horner Collaborator Loading…
1
chore: rename Equiv.Set.congr to Set.equivOfEq LLM-generated PRs with substantial input from LLMs - review accordingly t-data Data (lists, quotients, numbers, etc)
#43200 opened Aug 29, 2026 by YaelDillies Contributor Loading…
1
chore(CategoryTheory/Monoidal): scope □ and ⋔ notations
#43199 opened Aug 29, 2026 by robin-carlier Contributor Loading…
2
chore: remove all remaining flexible linter exceptions tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43198 opened Aug 29, 2026 by Parcly-Taxel Collaborator Loading…
1
feat(Order/Basic): relation properties of complement relations t-order Order theory
#43197 opened Aug 29, 2026 by SnirBroshi Collaborator Loading…
5
doc: add Jacobi Four-Square proof to the list of 1000 theorems new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#43196 opened Aug 28, 2026 by danderson70-UNL Contributor Loading…
3
feat(Algebra/Category/ModuleCat/Differentials): refactor the presheaf of differentials to use PresheafOfModulesOfCommRing large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43195 opened Aug 28, 2026 by Brian-Nugent Collaborator Loading…
1 task
4
ProTip! Adding no:label will show everything without a label.