Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,973 Open 38,377 Closed
2,973 Open 38,377 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(CategoryTheory): fix some nolint simpNF t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#41990 opened Jul 21, 2026 by felixpernegger Contributor Loading…
1
feat(NumberTheory/LegendreSymbol/QuadraticChar/Basic): characterize when products are squares 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-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41989 opened Jul 21, 2026 by bryan-hu Loading…
3
feat(FreeGroup): characterize commutative/cyclic free groups WIP Work in progress
#41988 opened Jul 21, 2026 by vlad902 Collaborator Loading…
1
feat: specific variations of Tendsto.smul when one of the limits is zero or one t-topology Topological spaces, uniform spaces, metric spaces, filters
#41987 opened Jul 21, 2026 by ADedecker Member Loading…
2
chore: update Mathlib dependencies 2026-07-21 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#41986 opened Jul 21, 2026 by mathlib-update-dependencies Bot Loading…
1
chore: split file Algebra.Lie.Algebra.Basis easy < 20s of review time. See the lifecycle page for guidelines. file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-algebra Algebra (groups, rings, fields, etc)
#41985 opened Jul 21, 2026 by ocfnash Contributor Loading…
1
fix: typo in simps error messages maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-meta Tactics, attributes or user commands
#41984 opened Jul 21, 2026 by fpvandoorn Member Loading…
3
fix(cache): avoid misleading message on refs not built "on purpose" CI Modifies the continuous integration setup or other automation
#41983 opened Jul 21, 2026 by marcelolynch Contributor • Draft
1
feat: generalize OpenPartialHomeomorph/IsImage to PartialHomeomorph awaiting-author A reviewer has asked the author a question or requested changes. t-topology Topological spaces, uniform spaces, metric spaces, filters
#41982 opened Jul 21, 2026 by scholzhannah Collaborator Loading…
@grunweg
5
refactor(Algebra/Polynomial): make into an abbrev of AddMonoidAlgebra tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#41981 opened Jul 21, 2026 by YaelDillies Contributor Loading…
1
feat(Analysis): the generalized hypergeometric function t-analysis Analysis (normed *, calculus)
#41980 opened Jul 21, 2026 by mcdoll Member • Draft
1
feat(LinearAlgebra/Matrix/GeneralLinearGroup/Card): add the theorem on the cardinality of the special linear group over a commring and over a finite field 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! t-algebra Algebra (groups, rings, fields, etc)
#41979 opened Jul 21, 2026 by Nicola9Falciola Contributor Loading…
1 task
3
feat(SetTheory/Cardinal): strong induction on Nat.card for finite types
#41978 opened Jul 21, 2026 by rosborn Contributor Loading…
1
refactor(simps): centralize notation_class and initialize_simps_projections large-import Automatically added label for PRs with a significant increase in transitive imports t-meta Tactics, attributes or user commands
#41976 opened Jul 21, 2026 by fpvandoorn Member Loading…
1
WIP large-import Automatically added label for PRs with a significant increase in transitive imports t-number-theory Number theory (also use t-algebra or t-analysis to specialize) WIP Work in progress
#41975 opened Jul 21, 2026 by fbarroero Collaborator Loading…
2
feat: products of bases of Lie algebras blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-algebra Algebra (groups, rings, fields, etc)
#41971 opened Jul 21, 2026 by ocfnash Contributor Loading…
1 of 2 tasks
2
feat(Topology): generalize Dieudonné's theorem to R1 spaces easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters
#41968 opened Jul 21, 2026 by peakpoint Collaborator Loading…
1
feat(Data/Set/Finite): Set.Finite.sigma t-data Data (lists, quotients, numbers, etc)
#41967 opened Jul 21, 2026 by peakpoint Collaborator Loading…
1
feat: ensure_constructive t-meta Tactics, attributes or user commands
#41966 opened Jul 21, 2026 by thorimur Contributor • Draft
1
ci: retire legacy zulip emoji workflows, enable emojis on mathlib4-nightly-testing CI Modifies the continuous integration setup or other automation file-removed A Lean module was (re)moved without a `deprecated_module` annotation LLM-generated PRs with substantial input from LLMs - review accordingly
#41965 opened Jul 21, 2026 by bryangingechen Contributor Loading…
1
feat(MeasureTheory/Integral): second mean value theorem for integration t-analysis Analysis (normed *, calculus) t-measure-probability Measure theory / Probability theory
#41964 opened Jul 21, 2026 by roos-j Collaborator Loading…
1
feat(AlgebraicTopology): nerve preserves products awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebraic-topology Algebraic topology
#41963 opened Jul 20, 2026 by sweeneyde Loading…
5
feat(Counterexamples): the space ω₁ new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#41962 opened Jul 20, 2026 by juanjomadrigal Loading…
6
feat(NumberTheory/Padics): abstract theory of measures, part II t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41961 opened Jul 20, 2026 by loefflerd Contributor Loading…
@MichaelStollBayreuth
2
chore(Topology/Order): cleanup imports t-topology Topological spaces, uniform spaces, metric spaces, filters
#41960 opened Jul 20, 2026 by qawbecrdtey Collaborator Loading…
4
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.