leanprover-community/mathlib3

Issues

• The Shapley-Folkman lemma

  #18135 opened 5 months ago by YaelDillies
  2

• Proof that the unit group of a number field is finitely-generated

  #18482 opened a year ago by riccardobrasca
  1

• Basics of tempered distributions

  #16386 opened 2 years ago by mcdoll
  1

• Define Hermite polynomials

  #15566 opened 2 years ago by mcdoll
  2

• Q: LLM and/or an RL agent trained on mathlib and tests

  #17919 opened 2 years ago by westurner
  1

• The ring of integers of a number field `K` is free of dimension `[K : ℚ]` / develop the theory of lattices

  #18150 opened 2 years ago by riccardobrasca
  3

• Lean 3.49.0 compatibility

  #17486 opened 2 years ago by tchajed
  6

• Link broken

  #18224 opened 2 years ago by RexRowan
  1

• Tracking: attribute semireducible/irreducible

  #18164 opened 2 years ago by jcommelin
  0

• Use a sensible sort order in multiset.repr

  #18166 opened 2 years ago by eric-wieser
  0

• Renaming `interval_oc` and `Ι a b`

  #17982 opened 2 years ago by winstonyin
  4

• mathlib/src/group_theory/presented_group.lean

  #18114 opened 2 years ago by jiajunma
  0

• Composition of convex functions

  #14902 opened 2 years ago by BoltonBailey
  1

• `(a :: l ++ [b]).last'` does not simplify to `some b`

  #18010 opened 2 years ago by jcpaik
  0

• Generalize `lower_semicontinuous_supr` and variations to *conditionally* complete linear orders

  #16940 opened 2 years ago by ADedecker
  0

• Refactor bilinear forms

  #15907 opened 2 years ago by mcdoll
  0

• `polyrith` fails if expression is an equality of numerals

  #17141 opened 2 years ago by eric-wieser
  0

• Diamond of complete boolean algebras on sets

  #16932 opened 2 years ago by ocfnash
  0

• backport remove with_cases

  #16568 opened 2 years ago by digama0
  0

• Pi is irrational

  #15860 opened 2 years ago by mcdoll
  5

• Connected components are open, under suitable hypotheses

  #15669 opened 2 years ago by hrmacbeth
  1

• backport remove `@[ext foo]`

  #16602 opened 2 years ago by digama0
  0

• evaluate `int.floor` and `int.fract` with `norm_num`

  #15992 opened 2 years ago by vihdzp
  2

• Lean is unable to infer `ordered_smul` instance from `pi.ordered_smul'`

  #16021 opened 2 years ago by apurvnakade
  1

• `obtain` without any deconstruction using a tactic block doesn't name hypotheses appropriately

  #15741 opened 2 years ago by ericrbg
  1

• Cleanup `direct_sum.sigma_curry` / `direct_sum.is_internal.collected_basis`

  #15756 opened 2 years ago by ADedecker
  0

• Remove `has_coe_to_fun` instance for `unitary_group`

  #15749 opened 2 years ago by mcdoll
  0

• Banach-Alaoglu for topological vector spaces

  #15734 opened 2 years ago by mcdoll
  0

• `expand_exists` improvements

  #15723 opened 2 years ago by robertylewis
  1

• Locally convex Hausdorff spaces

  #15565 opened 2 years ago by mcdoll
  0

• `has_continuous_inv₀` instance for `linear_ordered_field`

  #12781 opened 2 years ago by hrmacbeth
  1

• Add an instance `{add_,}sub{monoid,group}_class S M → has_coe_t S ({add_,}sub{monoid,group} M)`

  #15053 opened 2 years ago by Vierkantor
  0

• potential bug: same lean state but different outcomes from `simp`

  #15025 opened 2 years ago by nmtsy
  2

• apply' can close the goal with metavariables

  #14993 opened 2 years ago by fpvandoorn
  0

• nth_rewrite incorrectly unifies universe variables

  #14994 opened 2 years ago by fpvandoorn
  0

• Approximation tactic

  #14781 opened 2 years ago by BoltonBailey
  1

• mathlib does not work with lean 3.43.0

  #14234 opened 3 years ago by chenrui333
  6

• Integrability on intervals via exhausting them by smaller intervals

  #12666 opened 2 years ago by loefflerd
  2

• Create library note explaining seemingly redundant `fintype` and `decidable` arguments.

  #14275 opened 3 years ago by kmill
  1

• rename `geom_sum_pos_of_odd`

  #14123 opened 3 years ago by ericrbg
  3

• padic_norm file maintenance

  #13574 opened 3 years ago by BoltonBailey
  0

• convert `is_monoid_hom` etc to structures, and move out of deprecated

  #13506 opened 3 years ago by kim-em
  0

• `to_` framework

  #13461 opened 3 years ago by YaelDillies
  1

• simple_graph: Add graph isomorphism preserve walks and connectedness

  #13115 opened 3 years ago by Girgias
  1

• injective

  #12899 opened 3 years ago by jjaassoonn
  0

• Splitting `analysis.seminorm`

  #11894 opened 3 years ago by mcdoll
  0

• Finite nilpotent groups characterisations

  #11723 opened 3 years ago by nomeata
  1

• let `linear_combination` solve `≠` goals

  #12685 opened 3 years ago by hrmacbeth
  0

• let `linear_combination` subsume `ring`

  #11990 opened 3 years ago by hrmacbeth
  0

• `cauchy_seq.const_mul` fails to unify

  #12007 opened 3 years ago by ecstatic-morse
  1