-
Notifications
You must be signed in to change notification settings - Fork 1.3k
Pull requests: leanprover-community/mathlib4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
chore(CategoryTheory/Presentable/Directed): rename Category theory
exists_cardinal_directed.* -> ExistsCardinalDirected.*
t-category-theory
#39906
opened May 27, 2026 by
SnirBroshi
Collaborator
Loading…
chore(Order/CompleteBooleanAlgebra): dualize Order theory
symmDiff theorems
t-order
#39905
opened May 27, 2026 by
plp127
Contributor
Loading…
refactor(Analysis/Meromorphic): generalize 𝕜 → 𝕜 to 𝕜 → 𝕜' for order lemma when possible
t-analysis
Analysis (normed *, calculus)
#39904
opened May 27, 2026 by
wwylele
Collaborator
Loading…
feat(NumberTheory): add almost prime numbers
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)
#39903
opened May 27, 2026 by
akiezun
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/PSeries
codex
#39902
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation
codex
#39901
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral
codex
#39900
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/Normed/Unbundled/FiniteExtension
codex
#39899
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/Normed/Unbundled/AlgebraNorm
codex
#39898
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/Normed/Ring/Basic
codex
#39897
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/Normed/Operator/ContinuousLinearMap
codex
#39896
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/Normed/Module/MStructure
codex
#39895
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/Normed/Lp/WithLp
codex
#39894
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
refactor(Analysis): golf OpenAI Codex wrote (parts of) this PR.
LLM-generated
PRs with substantial input from LLMs - review accordingly
t-analysis
Analysis (normed *, calculus)
Mathlib/Analysis/Convex/Birkhoff
codex
#39893
opened May 27, 2026 by
yuanyi-350
Collaborator
Loading…
feat(GroupTheory/Commutator/Basic): more commutator identities
t-group-theory
Group theory
#39892
opened May 27, 2026 by
SnirBroshi
Collaborator
Loading…
feat(GroupTheory/Subgroup/Center): the center of a product is the product of the centers
awaiting-author
A reviewer has asked the author a question or requested changes.
t-group-theory
Group theory
#39891
opened May 26, 2026 by
SnirBroshi
Collaborator
Loading…
ci(decls-diff): post-build workflow that emits a Lean-aware diff into the step summary
CI
Modifies the continuous integration setup or other automation
#39888
opened May 26, 2026 by
adomani
Contributor
Loading…
ci(build_template): validate dump outputs are regular files before upload
CI
Modifies the continuous integration setup or other automation
#39887
opened May 26, 2026 by
adomani
Contributor
Loading…
chore(Geometry/Manifold): remove some Manifolds etc
tech debt
Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
@[expose] public section
t-differential-geometry
#39886
opened May 26, 2026 by
grunweg
Contributor
Loading…
refactor(GroupTheory/*): additivize Group theory
AddAut
t-group-theory
#39884
opened May 26, 2026 by
tb65536
Contributor
Loading…
chore(CategoryTheory/Functor): pointwise Kan extensions under isomorphisms
t-category-theory
Category theory
#39883
opened May 26, 2026 by
chrisflav
Member
Loading…
chore(CategoryTheory): Category theory
StructuredArrow.map₂ along equivalences induces an equivalence
t-category-theory
#39882
opened May 26, 2026 by
chrisflav
Member
Loading…
chore: decouple norm and algebra
slow-typeclass-synthesis
WIP
Work in progress
#39878
opened May 26, 2026 by
MichaelStollBayreuth
Contributor
Loading…
feat(ci): cross-reference tag review via post-build dump + workflow_run shim
blocked-by-other-PR
This PR depends on another PR (this label is automatically managed by a bot)
CI
Modifies the continuous integration setup or other automation
#39877
opened May 26, 2026 by
kim-em
Contributor
Loading…
1 task
Previous Next
ProTip!
Mix and match filters to narrow down what you’re looking for.