Issues
- 0
Tracking issue: Ordinal refactors
#17033 opened by vihdzp - 1
Tracking issue: remove references to List.nthLe
#12379 opened by grunweg - 1
A better notation for limit
#16794 opened by akp2003 - 0
Theory of smooth morphisms of schemes
#16890 opened by chrisflav - 0
general theory of Galois categories
#16670 opened by chrisflav - 1
wrong link for Complex.abs in documentation
#15415 opened by PhoenixIra - 3
Define hypergeometric functions
#15966 opened by ocfnash - 1
Rename `zpow_le_zpow` and `rpow_le_rpow`
#13544 opened by BoltonBailey - 0
Improving the performance of typeclass inference
#16644 opened by FR-vdash-bot - 5
abel_nf: PANIC at Lean.isLevelMVarAssignable Lean.MetavarContext:412:14: unknown universe metavariable
#15785 opened by eric-wieser - 4
lift tactic does not respect abbreviations
#15865 opened by jcommelin - 1
- 0
Math olympiad
#16023 opened by madvorak - 0
Performance regressions using `rintro` generally and `obtain` vs `rcases/have`
#15871 opened by mattrobball - 0
Proposal to add new attributes
#15509 opened by AdamSobieski - 0
Tracking issue for slow `field_simp` calls replaced by `simp`
#15486 opened by grunweg - 1
- 2
json: cannot unmarshal string into Go struct field lakeManifest.version of type int
#14222 opened by zhouliang-yu - 1
json: cannot unmarshal string into Go struct field lakeManifest.version of type int
#14259 opened by futureflsl - 0
norm_num for Nat.factors
#15410 opened by eric-wieser - 1
Building HTML documentation instructions fails on clean clone
#15369 opened by oeb25 - 1
PDE Support
#14784 opened by Adarsh321123 - 2
Formalization of PDEs in Lean?
#14685 opened by Robertboy18 - 0
fin_cases breaks on intervals of Fin
#14652 opened by shortc1rcuit - 0
Explode is incorrectly spaced when namespaces are open-ed
#14484 opened by advayDev1 - 1
The Shapley-Folkman lemma
#14427 opened by YaelDillies - 1
Data/Tree: Add `Traversable` instance.
#13572 opened by BoltonBailey - 0
- 2
`cc` tactic can't unify def-eq instances in `OfNat.ofNat`
#13362 opened by Komyyy - 0
Tracking issue: try replacing `measurability` by `fun_prop`
#13864 opened by grunweg - 0
`bibtool` not available in provided dev container
#13732 opened by StevenClontz - 2
slow typeclass synthesis: takes 19000 heartbeats to fail in `AddHomClass (AbsoluteValue ℂ ℝ) ?m ?m`
#12230 opened by kim-em - 2
slow typeclass synthesis: takes 15000 heartbeats in fail in `ZeroHomClass (Perm (Fin (Nat.succ n))) ?m ?m`
#12232 opened by kim-em - 2
- 0
General geometric representations of a Coxeter group
#13291 opened by trivial1711 - 0
`notation3` doesn't support unparenthesized multiple binders like `Π₀ i j, δ i j`
#13496 opened by Komyyy - 0
`lake exe cache get` should print a better "success" message.
#13276 opened by kim-em - 0
Regression after disabling `ConcreteCategory.instFunLike` as a global instance
#13342 opened by dagurtomas - 0
Broken link in mathlib4_docs
#13328 opened by matematiflo - 1
restore gh-problem-matcher-wrap in CI
#12946 opened by kim-em - 1
`#where` doesn't print `open scoped`
#12606 opened by fpvandoorn - 1
- 0
`IsCompact.exists_forall_ge` is deprecated, but widely used
#12774 opened by kim-em - 0
- 0
Porting note: `simp` doesn't apply `simp` lemma unless parenthesized
#12717 opened by Ruben-VandeVelde - 1
Doc site is not rendering equations of probability theory
#12681 opened by linonetwo - 0
- 0
- 0
Support `Fact` for the `slim_check` tactic
#12565 opened by grhkm21 - 0
simps: generate all lemmas but one
#12564 opened by fpvandoorn