Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,742 Open 37,915 Closed
2,742 Open 37,915 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: implement LMFDB attribute t-meta Tactics, attributes or user commands WIP Work in progress
#41290 opened Jul 2, 2026 by Paul-Lez Collaborator Loading…
1
feat(Dynamics): recurrents set and refactoring of conservative maps t-dynamics Dynamical Systems
#41289 opened Jul 2, 2026 by D-Thomine Collaborator • Draft
1
feat(EReal): add_eq_top_iff_eq_top_* t-data Data (lists, quotients, numbers, etc)
#41288 opened Jul 2, 2026 by lua-vr Contributor Loading…
1
feat(EReal): addition of real as an orderIso t-topology Topological spaces, uniform spaces, metric spaces, filters
#41286 opened Jul 2, 2026 by lua-vr Contributor Loading…
1
feat(AlgebraicTopology/SimplicialSet): relative homology blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology WIP Work in progress
#41285 opened Jul 2, 2026 by joelriou Contributor Loading…
1 task
2
feat(InnerProductSpace): facts about invarant functions and coboundaries large-import Automatically added label for PRs with a significant increase in transitive imports
#41284 opened Jul 2, 2026 by lua-vr Contributor • Draft
1
feat(Tactic/ComputablePolynomial): computable multivariate polynomials and mv_decide t-meta Tactics, attributes or user commands
#41283 opened Jul 2, 2026 by mkaratarakis Contributor • Draft
1
feat(Tactic/ComputablePolynomial): computable univariate polynomials and poly_decide t-meta Tactics, attributes or user commands
#41282 opened Jul 2, 2026 by mkaratarakis Contributor • Draft
1
doc(NumberTheory/ModularForms): remove a TODO which is done easy < 20s of review time. See the lifecycle page for guidelines. t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41281 opened Jul 2, 2026 by loefflerd Contributor Loading…
2
feat(Geometry/Manifold): C^n smoothness of the inverse of a bundle trivialization t-differential-geometry Manifolds etc
#41280 opened Jul 2, 2026 by Deicyde Contributor Loading…
2
feat(NumberTheory): the identity of the abstract Hecke ring t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41279 opened Jul 2, 2026 by CBirkbeck Collaborator • Draft
1
chore(RepresentationTheory/Character): golf some results in FDRep maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)
#41278 opened Jul 2, 2026 by Yu-Misaka Collaborator Loading…
10
feat(NumberTheory): the convolution product on abstract Hecke rings t-group-theory Group theory
#41277 opened Jul 2, 2026 by CBirkbeck Collaborator • Draft
1
chore: remove simple nonrec occurences blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#41276 opened Jul 2, 2026 by felixpernegger Contributor Loading…
1 task
5
chore(Algebra/Module/Submodule/Ker): state injective_domRestrict_iff with Disjoint LLM-generated PRs with substantial input from LLMs - review accordingly
#41275 opened Jul 2, 2026 by kim-em Contributor • Draft
5
feat(Order/ConditionallyCompleteLattice): antitone versions of sSup (f '' s) lemmas t-order Order theory
#41273 opened Jul 2, 2026 by SnirBroshi Collaborator Loading…
1
chore(LinearAlgebra/Matrix/Nondegenerate): generalize lemmas to CommSemiring LLM-generated PRs with substantial input from LLMs - review accordingly maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)
#41271 opened Jul 2, 2026 by kim-em Contributor Loading…
7
refactor(Combinatorics/SimpleGraph/CycleGraph): golf cycleGraph_isContained_iff via getVert LLM-generated PRs with substantial input from LLMs - review accordingly t-combinatorics Combinatorics
#41268 opened Jul 2, 2026 by kim-em Contributor • Draft
1
refactor(Archive/Imo/Imo2000Q2): replace SOS certificate with classical AM-GM argument IMO Math olympiad problems LLM-generated PRs with substantial input from LLMs - review accordingly
#41267 opened Jul 2, 2026 by kim-em Contributor • Draft
2
feat(EllipticCurve/Affine/Point): easy instances easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry
#41264 opened Jul 2, 2026 by alreadydone Contributor Loading…
1
refactor(Archive/Imo/Imo2000Q2): unify helper lemma orderings IMO Math olympiad problems LLM-generated PRs with substantial input from LLMs - review accordingly
#41263 opened Jul 2, 2026 by kim-em Contributor • Draft
2
feat(Algebra/Group/Subgroup/ZPowers/Lemmas): zmultiples sup/inf over the integers easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#41261 opened Jul 2, 2026 by SnirBroshi Collaborator Loading…
1
feat(GroupTheory/Exponent): the order of a group divides a power of its exponent awaiting-author A reviewer has asked the author a question or requested changes. large-import Automatically added label for PRs with a significant increase in transitive imports t-group-theory Group theory
#41260 opened Jul 2, 2026 by SnirBroshi Collaborator Loading…
2
chore: remove redudant nonrec's
#41259 opened Jul 1, 2026 by felixpernegger Contributor Loading…
3
feat(Analysis/Fourier/FiniteAbelian): add the Donoho-Stark support uncertainty principle 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-analysis Analysis (normed *, calculus)
#41258 opened Jul 1, 2026 by ungatz Loading…
5 tasks done
5
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.