Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,428 Open 35,742 Closed
2,428 Open 35,742 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: use alias_in attribute for CW complexes t-topology Topological spaces, uniform spaces, metric spaces, filters
#38785 opened Apr 30, 2026 by scholzhannah Collaborator Loading…
1
feat(Algebra/Algebra/RestrictScalars): Generalize RestrictScalars WIP Work in progress
#38784 opened Apr 30, 2026 by justus-springer Collaborator Loading…
2
experiment / do not review: breaking change for downstream t-measure-probability Measure theory / Probability theory
#38783 opened Apr 30, 2026 by marcelolynch Contributor Loading…
2
chore(RingTheory/IntegralClosure/IsIntegralClosure/Basic): clean up variables t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38782 opened Apr 30, 2026 by tb65536 Contributor Loading…
1
feat: instance diamond linter t-linter Linter
#38781 opened Apr 30, 2026 by JovanGerb Contributor • Draft
2
chore(Catalogue PR): kill some erws by adding rfl lemmas
#38780 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(Topology/Category): replace TopCat by TopCat.{u} LLM-generated PRs with substantial input from LLMs - review accordingly t-category-theory Category theory WIP Work in progress
#38779 opened Apr 30, 2026 by chrisflav Member Loading…
@dagurtomas
8
feat(Topology/EMetricSpace): instances of weak extended metric spaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#38778 opened Apr 30, 2026 by felixpernegger Contributor Loading…
1
feat(Algebra/Module/RingHom): add Module.compHom_smul_def 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)
#38777 opened Apr 30, 2026 by JJYYY-JJY Contributor Loading…
5
feat(Topology): Skyscraper sheaves are flasque t-topology Topological spaces, uniform spaces, metric spaces, filters
#38775 opened Apr 30, 2026 by Raph-DG Collaborator Loading…
1
chore(NumberTheory/Padics/Complex): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38774 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(MeasureTheory/Measure/Haar/Quotient): remove erws codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-measure-probability Measure theory / Probability theory
#38773 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(LinearAlgebra/TensorProduct/Subalgebra): remove erws codex OpenAI Codex wrote (parts of) this PR. 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)
#38772 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
4
chore(LinearAlgebra/Eigenspace/Basic): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-algebra Algebra (groups, rings, fields, etc)
#38771 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(LinearAlgebra/AffineSpace/Combination): remove an erw codex OpenAI Codex wrote (parts of) this PR. easy < 20s of review time. See the lifecycle page for guidelines. 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)
#38770 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
3
chore(GroupTheory/FreeGroup/NielsenSchreier): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-group-theory Group theory
#38769 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(Condensed/Light/Epi): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-condensed Condensed mathematics
#38768 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
3
chore(Analysis/Fourier/FourierTransformDeriv): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly
#38767 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(AlgebraicTopology/DoldKan/GammaCompN): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-algebraic-topology Algebraic topology
#38766 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
2
chore(AlgebraicGeometry/Restrict): remove erws codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-algebraic-geometry Algebraic geometry
#38765 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(AlgebraicGeometry/Modules/Tilde): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-algebraic-geometry Algebraic geometry
#38764 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(AlgebraicGeometry/GammaSpecAdjunction): remove an erw codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-algebraic-geometry Algebraic geometry
#38763 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(AlgebraicGeometry/EllipticCurve/Projective/Point): remove erws codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-algebraic-geometry Algebraic geometry
#38762 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
chore(AlgebraicGeometry/EllipticCurve/Jacobian/Point): remove erws codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-algebraic-geometry Algebraic geometry
#38761 opened Apr 30, 2026 by yuanyi-350 Collaborator Loading…
1
feat: use Cartan's criterion for semisimplicty to drop redundant hypotheses t-algebra Algebra (groups, rings, fields, etc)
#38760 opened Apr 30, 2026 by ocfnash Contributor Loading…
2
ProTip! Filter pull requests by the default branch with base:master.