Task browser
Every theorem in the benchmark
Held-out theorems come from Mathlib modules that almost nothing imports; their proofs may not use anything from that module or from modules built on it. Authored theorems were written for this project and each has a certified reference proof.
203 of 203 theorems
- mh_cate_94f544Category theoryeasyMathlib held-out✕ unsolved (15 configs)
: (CategoryTheory.MorphismProperty.monomorphisms (Type u)).IsStableUnderCobaseChange - mh_cate_ea624fCategory theoryeasyMathlib held-out✓ solved by 10/15
{α : Type u_1} [Preorder α] {i j : α} (h : i ≤ j) : Set.initialSegIicIicOfLE h = Set.initialSegIicIicOfLE h - mh_cate_9a8e08Category theoryhardMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.Limits.PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda - mh_cate_6496c7Category theorymediumMathlib held-out✕ unsolved (15 configs)
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) : G.IsSplitPair (F.map A.a) (adj.counit.app (F.obj A.A)) - mh_cate_431372Category theorymediumMathlib held-out✕ unsolved (15 configs)
(G : Type u) [Group G] [Finite G] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat - mh_cate_cd9a3bCategory theoryhardMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.HasLeftCalculusOfFractions - mh_cate_097148Category theorymediumMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveYoneda.obj X) - mh_cate_640afdCategory theorymediumMathlib held-out✓ solved by 1/15
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {sq : CategoryTheory.Square C} (h : sq.IsPullback) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback - mh_cate_b3526cCategory theorymediumMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] {A B I Z : C} (i : A ⟶ B) [CategoryTheory.Mono i] [CategoryTheory.Injective I] (p : I ⟶ Z) (hZ : CategoryTheory.Limits.IsZero Z) : CategoryTheory.HasLiftingProperty i p - mh_cate_15119dCategory theorymediumMathlib held-out✕ unsolved (15 configs)
{C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj - mh_cate_f827c0Category theoryeasyMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] : CategoryTheory.HasProjectiveResolutions C - mh_cate_a78895Category theoryeasyMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : CategoryTheory.HasSubobjectClassifier (CategoryTheory.Functor Cᵒᵖ (Type w)) - mh_cate_b720d5Category theoryeasyMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (R : CategoryTheory.ProjectiveResolution X) : R.cochainComplex.IsKProjective - mh_cate_63c919Category theoryhardMathlib held-out✕ unsolved (15 configs)
{X : Type u} {κ : Cardinal.{u}} (hX : HasCardinalLT X κ) [Fact κ.IsRegular] : CategoryTheory.IsCardinalPresentable X κ - mh_cate_7a05c0Category theoryhardMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [Fact κ.IsRegular] [CategoryTheory.IsCardinalAccessibleCategory C κ] (X : C) : CategoryTheory.IsCardinalFiltered (CategoryTheory.CostructuredArrow (CategoryTheory.isCardinalPresentable C κ).ι X) κ - mh_cate_a4e517Category theorymediumMathlib held-out✕ unsolved (15 configs)
{G : Type v} [Group G] [Finite G] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) FintypeCat.incl - mh_cate_5dd50cCategory theorymediumMathlib held-out✕ unsolved (15 configs)
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.snd - mh_cate_643c86Category theoryhardMathlib held-out✕ unsolved (15 configs)
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) : Nonempty (CategoryTheory.Limits.IsLimit (E.toPreOneHypercover.multifork F)) ↔ CategoryTheory.Presieve.IsSheafFor F E.presieve₀ - mh_cate_79488eCategory theoryeasyMathlib held-out✕ unsolved (15 configs)
(w : CategoryTheory.uliftFunctor.{u, v}.EssSurj) : UnivLE.{max u v, v} - mh_cate_bb5cedCategory theorymediumMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : (CategoryTheory.MorphismProperty.coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp - mh_cate_f66b15Category theoryeasyMathlib held-out · devnot attempted
{J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasLimitsOfShape J FintypeCat - mh_cate_da18c0Category theoryeasyMathlib held-out · devnot attempted
{M : Type u_1} [MulOneClass M] {S T : Submonoid M} (h : S ≤ T) : Submonoid.inclusion h = Submonoid.inclusion h - mh_cate_660828Category theorymediumMathlib held-out · devnot attempted
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] {f : X ⟶ Y} (w : f ≠ 0) : CategoryTheory.IsIso f - mh_cate_5ea941Category theoryeasyMathlib held-out · devnot attempted
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities] [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts] : CategoryTheory.Limits.HasFiniteProducts W.Localization - mh_cate_3aecb1Category theorymediumMathlib held-out · devnot attempted
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) : F.IsCosplitPair (G.map A.a) (adj.unit.app (G.obj A.A)) - mh_prob_18b249ProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (t : ℝ) (hX : AEMeasurable X μ) : MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * X ω)) μ - mh_prob_9960e2ProbabilityhardMathlib held-out✕ unsolved (15 configs)
{Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht_int_pos : MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ) (ht_int_neg : MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ) : MeasureTheory.Integrable (fun ω => Real.exp (|t| * |X ω|)) μ - mh_prob_e9d147ProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (ProbabilityTheory.mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ - mh_prob_7d2670ProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E} [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] (hX : ProbabilityTheory.HasGaussianLaw X P) : MeasureTheory.Integrable X P - mh_prob_51c110ProbabilitymediumMathlib held-out✕ unsolved (15 configs)
(r : NNReal) : HasSum (fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) 1 - mh_prob_4476a9ProbabilityeasyMathlib held-out✕ unsolved (15 configs)
: LawfulMonad PMF - mh_prob_3344fdProbabilityhardMathlib held-out✕ unsolved (15 configs)
{y z : ℝ} (f : ℝ → ENNReal) (hzy : z ≤ y) : ∫⁻ (x : ℝ) in Set.Iic y, f x = (∫⁻ (x : ℝ) in Set.Iio z, f x) + ∫⁻ (x : ℝ) in Set.Icc z y, f x - mh_prob_9ba5afProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{b x : ℝ} (hb : 0 < b) : MeasureTheory.IntegrableOn (fun x => Real.exp (-(b * x))) (Set.Ioc 0 x) MeasureTheory.volume - mh_prob_d34b98ProbabilityhardMathlib held-out✕ unsolved (15 configs)
{p : ℕ → ℝ} {r : ℝ} (k : ℕ) (hr : Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r)) : Filter.Tendsto (fun n => ↑(n.choose k) * p n ^ k) Filter.atTop (nhds (r ^ k / ↑k.factorial)) - mh_prob_6d9dc4ProbabilityhardMathlib held-out✕ unsolved (15 configs)
{β : Type u_1} [LinearOrder β] {t : ℕ → β} (ht_mono : StrictMono t) (ht_tendsto : Filter.Tendsto t Filter.atTop Filter.atTop) {x : β} (hx : t 0 < x) : ∃ n, t n < x ∧ x ≤ t (n + 1) - mh_prob_eba19eProbabilityhardMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : Measurable fun a => (κ a).singularPart (η a) - mh_prob_dbcf26ProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E] (h : ∀ (x : E), μ ≠ MeasureTheory.Measure.dirac x) : MeasureTheory.NullSingletonClass μ - mh_prob_98303dProbabilityhardMathlib held-out✕ unsolved (15 configs)
{Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {a b t : ℝ} (hm : AEMeasurable X μ) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) : MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ - mh_prob_171948ProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × ℝ)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsRatCondKernelCDF (fun p q => κ.density κ.fst p.1 p.2 (Set.Iic ↑q)) κ κ.fst - mh_prob_741109ProbabilityhardMathlib held-out✕ unsolved (15 configs)
(x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) : |x| ^ p ≤ (p / |t|) ^ p * max (Real.exp (t * x)) (Real.exp (-t * x)) - mh_prob_381e5eProbabilityeasyMathlib held-out✕ unsolved (15 configs)
{Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOn ℝ (ProbabilityTheory.cgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ)) - mh_prob_7642f8ProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E} [NormedSpace ℝ E] (hX : ProbabilityTheory.HasGaussianLaw X P) : ProbabilityTheory.HasGaussianLaw (-X) P - mh_prob_65591aProbabilityeasyMathlib held-out✕ unsolved (15 configs)
(r : NNReal) : HasSum (fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) 1 - mh_prob_ed4cc9ProbabilityeasyMathlib held-out✕ unsolved (15 configs)
: LawfulFunctor PMF - mh_prob_31af9cProbabilitymediumMathlib held-out✕ unsolved (15 configs)
{r x : ℝ} : HasDerivAt (fun a => -Real.exp (-(r * a))) (r * Real.exp (-(r * x))) x - mh_prob_4b5727ProbabilityhardMathlib held-out · devnot attempted
{Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) : ∫ (ω : Ω), 1 - X ω ∂μ = μ.real {ω | X ω = 0} - mh_prob_1ffcf9ProbabilityhardMathlib held-out · devnot attempted
{E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] {p : ENNReal} (h_Lp : MeasureTheory.MemLp (fun x => x - ∫ (y : E), y ∂μ) p μ) : MeasureTheory.MemLp id p μ - mh_prob_ec6bfeProbabilityhardMathlib held-out · devnot attempted
{Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} (ht : t ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (p : NNReal) : MeasureTheory.MemLp X (↑p) (μ.tilted fun x => t * X x) - mh_prob_4c0e75ProbabilityhardMathlib held-out · devnot attempted
{Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) : ∫ (x : Ω), X x ∂μ = μ.real {ω | X ω = 1} - mh_prob_59ac72ProbabilityhardMathlib held-out · devnot attempted
{Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} (ht : t ∈ interior (ProbabilityTheory.integrableExpSet X μ)) : (∫ (x : Ω), X x ∂μ.tilted fun x => t * X x) = deriv (ProbabilityTheory.cgf X μ) t - mh_func_75745eFunctionsmediumMathlib held-out✕ unsolved (15 configs)
{G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : StrictAntiOn f (Set.Ici 0)) : StrictAnti f - mh_func_e6d870FunctionseasyMathlib held-out✓ solved by 1/15
: Function.RightInverse not not - mh_func_362ff8FunctionshardMathlib held-out✕ unsolved (15 configs)
{G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : MonotoneOn f (Set.Ici 0)) : Monotone f - mh_func_7a8899FunctionseasyMathlib held-out✓ solved by 1/15
: Function.Injective not - mh_func_19daffFunctionshardMathlib held-out✕ unsolved (15 configs)
{G : Type u_1} {H : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup H] [PartialOrder H] [IsOrderedAddMonoid H] {f : G → H} (h₁ : ∀ (x : G), f (-x) = -f x) (h₂ : StrictMonoOn f (Set.Ici 0)) : StrictMono f - mh_func_671ad9FunctionseasyMathlib held-out✓ solved by 1/15
: Function.Bijective not - mh_ineq_664419InequalitieseasyMathlib held-out✕ unsolved (15 configs)
{α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [LE β] [Zero β] {v₁ : α₁ → β} {v₂ : α₂ → β} : 0 ≤ Sum.elim v₁ v₂ ↔ 0 ≤ v₁ ∧ 0 ≤ v₂ - mh_ineq_7f6f03InequalitieseasyMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] (f : α →+*o α) : f = OrderRingHom.id α - mh_ineq_fea870InequalitieseasyMathlib held-out✕ unsolved (15 configs)
{n a : ℕ} : (∃ x, x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a - mh_ineq_040adcInequalitieshardMathlib held-out✕ unsolved (15 configs)
{R : Type u_1} {S : Type u_2} [LinearOrder R] [LinearOrder S] [CommRing R] [IsStrictOrderedRing R] [Ring S] [IsStrictOrderedRing S] [DenselyOrdered R] [Archimedean R] {x y : S} (f : R →+* S) (hf : StrictMono ⇑f) : ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔ ∃ q, 0 < f q ∧ f q * |y| ≤ |x| - mh_ineq_5013c9InequalitieseasyMathlib held-out✓ solved by 7/15
(R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] : Subsemiring.nonneg R = Subsemiring.nonneg R - mh_ineq_4598e8InequalitiesmediumMathlib held-out✕ unsolved (15 configs)
: StrictConcaveOn ℝ (Set.Ici 0) fun x => √x - mh_ineq_8c7304InequalitieshardMathlib held-out✕ unsolved (15 configs)
{K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {x : K} {m n : ℕ} (hx : 0 ≤ x) (h'x : x < 1) : ∑ i ∈ Finset.Ico m n, x ^ i ≤ x ^ m / (1 - x) - mh_ineq_f31a9aInequalitieseasyMathlib held-out✕ unsolved (15 configs)
(x : ENNReal) (y : ℝ) : x ^ y = (↑y * x.log).exp - mh_ineq_8efe00InequalitiesmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [Add ι] [One ι] [SuccAddOrder ι] [NoMaxOrder ι] (f : ι → α) (i : ι) : disjointed f (i + 1) = f (i + 1) \ (partialSups f) i - mh_ineq_910a5cInequalitieshardMathlib held-out✓ solved by 9/15
(Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Archimedean R] [Nontrivial R] : HahnSeries.archimedeanClassOrderIsoWithTop Γ R = HahnSeries.archimedeanClassOrderIsoWithTop Γ R - mh_ineq_86eb8eInequalitiesmediumMathlib held-out✕ unsolved (15 configs)
{ι : Type u_1} {G : Type u_2} [AddGroup G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G} [AddLeftMono G] (hf : BddAbove (Set.range f)) (a : G) : a + ⨆ i, f i = ⨆ i, a + f i - mh_ineq_be9cc2InequalitieseasyMathlib held-out✓ solved by 3/15
{R : Type u_1} [CommRing R] {P₁ P₂ : RingPreordering R} : ↑P₁ < ↑P₂ ↔ P₁ < P₂ - mh_ineq_ab1d8aInequalitieseasyMathlib held-out✕ unsolved (15 configs)
(c : ℝ) : (fun x => Real.log (x * c)) =O[Filter.atTop] Real.log - mh_ineq_9165bfInequalitieshardMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {β : Type u_2} [Preorder α] [Add α] [Sub α] [OrderedSub α] [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : α →ₙ+ β) (hf : Monotone ⇑f) (a b : α) : f a - f b ≤ f (a - b) - mh_ineq_04b8caInequalitiesmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_2} [LinearOrder α] [One α] [Sub α] [PredSubOrder α] {b : α} (hb : ¬IsMin b) : Set.Iic (b - 1) = Set.Iio b - mh_ineq_2410e2InequalitiesmediumMathlib held-out✕ unsolved (15 configs)
{ι : Type u_1} {α : Type u_2} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] {f g : ι → α} [Fintype ι] (hfg : Antivary f g) : ↑(Fintype.card ι) * ∑ i, f i * g i ≤ (∑ i, f i) * ∑ i, g i - mh_ineq_f31eb9InequalitieshardMathlib held-out✕ unsolved (15 configs)
{α : Type u_2} [Field α] [ConditionallyCompleteLinearOrder α] [IsStrictOrderedRing α] : Archimedean α - mh_ineq_32dd0aInequalitiesmediumMathlib held-out✕ unsolved (15 configs)
{ι : Type u_1} {f : ι → ℂ} (hf : Summable f) : Summable fun i => Complex.log (1 + f i) - mh_ineq_044d16InequalitieshardMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) : Multiset.map (fun x => c + x) (Multiset.Icc a b) = Multiset.Icc (c + a) (c + b) - mh_ineq_489bb6InequalitieseasyMathlib held-out✓ solved by 5/15
(M : Type u_1) [Monoid M] [Preorder M] [MulLeftMono M] : Submonoid.oneLE M = Submonoid.oneLE M - mh_ineq_a3c705InequalitieseasyMathlib held-out · devnot attempted
{M : Type u_1} [Monoid M] [LE M] [MulLeftMono M] (u : Mˣ) {a b : M} : a ≤ ↑u⁻¹ * b → ↑u * a ≤ b - mh_ineq_3d5b16InequalitiesmediumMathlib held-out · devnot attempted
{ι : Type u_1} [DecidableEq ι] {s : Finset ι} (n : ℕ) : (s.finsuppAntidiag n).card = s.card.multichoose n - mh_ineq_c08241InequalitiesmediumMathlib held-out · devnot attempted
{α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [AddGroup α] [Preorder ι] [LocallyFiniteOrderBot ι] [AddRightMono α] (f : ι → α) (c : α) (i : ι) : (partialSups fun x => f x + c) i = (partialSups f) i + c - mh_ineq_6cb696InequalitieshardMathlib held-out · devnot attempted
{M : Type u_1} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedMul M] : WellFoundedGT (SemigroupIdeal M) - mh_ineq_a0ad18InequalitiesmediumMathlib held-out · devnot attempted
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Set α} {a ε : α} (h : IsLUB s a) (hε : 0 < ε) : ∃ b ∈ s, a - ε < b ∧ b ≤ a - mh_sets_42f697SetsmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset α → β} : Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (Finset.cons a s ha) - mh_sets_3ff207SetsmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} [LinearOrder α] [DenselyOrdered α] {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y - mh_sets_2851bfSetsmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {ι : Type u_2} [Finite ι] {s : ι → Set α} (hs : Pairwise (Function.onFun Disjoint s)) : (⋃ i, s i).encard = ∑ᶠ (i : ι), (s i).encard - mh_sets_82aa9bSetseasyMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {s t : Finset α} : s ⋖ t → s.val ⋖ t.val - mh_sets_4267d0SetsmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u} {β : Type v} (f : Set (α → β)) (s : Set α) [Finite ↑f] [Finite ↑s] : Finite ↑(f.seq s) - mh_sets_80248aSetsmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset α → β} [DecidableEq α] : StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s) - mh_sets_2edc70SetshardMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} [LinearOrder α] [DenselyOrdered α] {s t : Set α} (hsf : s.Finite) (hs : s.Nonempty) (htf : t.Finite) (ht : t.Nonempty) (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y - mh_sets_371d21SetshardMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {s : Set α} : ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard - mh_sets_64ee0aSetseasyMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {s t : Finset α} (h : s ⋖ t) : s.card ⋖ t.card - mh_sets_2a659fSetseasyMathlib held-out✓ solved by 2/15
{α β : Type u} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) : (f <*> s).Finite - mh_sets_572f4eSetsmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset α → β} [DecidableEq α] : Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s) - mh_sets_92d1e1SetshardMathlib held-out✓ solved by 7/15
{α : Type u_1} [LinearOrder α] [DenselyOrdered α] (s t : Finset α) [NoMaxOrder α] [NoMinOrder α] [Nonempty α] (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y - mh_sets_dc1cd2SetsmediumMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {ι : Type u_2} (t : Finset ι) (s : ι → Set α) : (⋃ i ∈ t, s i).ncard ≤ ∑ i ∈ t, (s i).ncard - mh_sets_8f88f1SetseasyMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s - mh_sets_185b9aSetseasyMathlib held-out✕ unsolved (15 configs)
{α : Type u} {β : Type v} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) : (f.seq s).Finite - mh_sets_77230dSetsmediumMathlib held-out · devnot attempted
{α : Type u_1} {β : Type u_2} {c : Set (Set α)} (hc : IsChain (fun x1 x2 => x1 ⊆ x2) c) [PartialOrder β] [OrderBot β] (f : α → β) : (⋃ s ∈ c, s).PairwiseDisjoint f ↔ ∀ s ∈ c, s.PairwiseDisjoint f - mh_sets_86d70fSetseasyMathlib held-out · devnot attempted
{α : Type u_1} {β : Type u_2} {c : Set (Set α)} (hc : IsChain (fun x1 x2 => x1 ⊆ x2) c) [PartialOrder β] [OrderBot β] (f : α → β) : (⋃₀ c).PairwiseDisjoint f ↔ ∀ s ∈ c, s.PairwiseDisjoint f - mh_sets_921469SetseasyMathlib held-out · devnot attempted
{p : ℕ} (hp : Nat.Prime p) : (p ^ 2).divisors = {p ^ 2, p, 1} - mh_sets_977709SetsmediumMathlib held-out · devnot attempted
{α : Type u_1} {c : Set (Set α)} {r : α → α → Prop} (hc : IsChain (fun x1 x2 => x1 ⊆ x2) c) : (⋃ s ∈ c, s).Pairwise r ↔ ∀ s ∈ c, s.Pairwise r - mh_numb_ca43f0Number theoryhardMathlib held-out✕ unsolved (15 configs)
{x : ℝ} (hx : 1 < x) : ↑⌊x⌋₊.primeCounting ≤ Real.log 4 * x / Real.log √x + √x - mh_numb_215e3bNumber theoryhardMathlib held-out✕ unsolved (15 configs)
{R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : 1 < Ideal.absNorm v.asIdeal - mh_numb_3b08d7Number theoryhardMathlib held-out✕ unsolved (15 configs)
{τ : ℂ} (hτ : 0 < τ.im) (n : ℤ) : ‖Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * τ)‖ ≤ Real.exp (-Real.pi * τ.im) ^ n.natAbs - mh_numb_a0ce52Number theoryhardMathlib held-out✕ unsolved (15 configs)
{n : ℕ} (hn : Even n) : AddSubmonoid.closure (Set.range fun x => x ^ n) = AddSubmonoid.nonneg ℤ - mh_numb_0f4d04Number theoryeasyMathlib held-out✓ solved by 6/15
{K : Type u_1} [Field K] {v : NumberField.InfinitePlace K} (hv : v.IsComplex) : NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv = NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv - mh_numb_b64eacNumber theorymediumMathlib held-out✕ unsolved (15 configs)
(n : ℕ) : ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n - mh_numb_7d6af5Number theorymediumMathlib held-out✕ unsolved (15 configs)
{N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun x => Φ ↑x) s - mh_numb_92dc99Number theorymediumMathlib held-out✕ unsolved (15 configs)
{K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] (k : Subfield K) : Algebra.IsAlgebraic (↥k) K - mh_numb_19a1f5Number theorymediumMathlib held-out✕ unsolved (15 configs)
(n : ℕ) : Real.log ↑(n + 1) ≤ ↑(harmonic n) - mh_numb_7e1e07Number theoryeasyMathlib held-out✕ unsolved (15 configs)
: IsTrans ℕ fun a b => b + 2 ≤ a - mh_numb_6c2443Number theoryhardMathlib held-out✕ unsolved (15 configs)
{E : Type u_1} [SeminormedAddCommGroup E] {f : UpperHalfPlane → E} (hf_cont : Continuous f) (hf_infinity : UpperHalfPlane.IsBoundedAtImInfty f) (hf_inv : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), f (g • τ) = f τ) : ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C - mh_numb_aac668Number theoryeasyMathlib held-out✕ unsolved (15 configs)
{a b : ℤ} : a.natAbs = b.natAbs ↔ a * a = b * b - mh_numb_7e8d93Number theoryhardMathlib held-out✕ unsolved (15 configs)
{N : ℕ} [NeZero N] {R : Type u_1} [CommRing R] (e : AddChar (ZMod N) R) (χ : DirichletCharacter R N) {d : ℕ} (hd : d ∣ N) (he : e.mulShift ↑d = 1) {u : (ZMod N)ˣ} (hu : (ZMod.unitsMap hd) u = 1) : χ ↑u * gaussSum χ e = gaussSum χ e - mh_numb_8ae352Number theoryhardMathlib held-out✕ unsolved (15 configs)
{Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (hΓ : ∃ h ∈ Γ.strictPeriods, 0 < h) {a b : ℤ} {f : ModularForm Γ a} {g : ModularForm Γ b} (hf : f ≠ 0) (hg : g ≠ 0) : f.mul g ≠ 0 - mh_numb_bcedf7Number theoryeasyMathlib held-out✕ unsolved (15 configs)
(M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nat.card (MulChar M R) = Nat.card Mˣ - mh_numb_485b85Number theoryhardMathlib held-out✕ unsolved (15 configs)
{p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] (f : C(ℤ_[p], E)) : Filter.Tendsto (fun x => (fwdDiff 1)^[x] (⇑f) 0) Filter.atTop (nhds 0) - mh_numb_35bfb0Number theoryhardMathlib held-out✕ unsolved (15 configs)
{k : ℕ} (n : ℕ) (hk0 : k ≠ 0) : ∃ p, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k] - mh_numb_4bec63Number theoryeasyMathlib held-out✕ unsolved (15 configs)
: StrictMonoOn Int.natAbs (Set.Ici 0) - mh_numb_4094ceNumber theoryhardMathlib held-out✕ unsolved (15 configs)
{k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.hurwitzZeta (↑x) (-↑k) = -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) - mh_numb_06c796Number theoryeasyMathlib held-out✕ unsolved (15 configs)
(z : ZMod 4) : z * z ≠ 2 - mh_numb_b61e4dNumber theoryeasyMathlib held-out · devnot attempted
(q : ℚ) : IsAlgebraic ℤ (Real.tan (↑q * Real.pi)) - mh_numb_671a3bNumber theorymediumMathlib held-out · devnot attempted
(hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem - mh_numb_0e8287Number theoryeasyMathlib held-out · devnot attempted
{p : ℕ} (h : Nat.Prime p) : ¬p.Perfect - mh_numb_b96188Number theoryhardMathlib held-out · devnot attempted
{n : ℕ} (hn : 1 < n) (hpn : ¬IsPrimePow n) : (Finset.Icc 1 (n - 1)).gcd n.choose = 1 - mh_numb_0a85d7Number theoryeasyMathlib held-out · devnot attempted
(f : ℕ → ℂ) : AnalyticOn ℂ (LSeries f) {s | LSeries.abscissaOfAbsConv f < ↑s.re} - mh_alge_32983eAlgebramediumMathlib held-out✕ unsolved (15 configs)
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Epi f] (X : Cᵒᵖ) : CategoryTheory.Epi (f.app X) - mh_alge_c62440AlgebrahardMathlib held-out✕ unsolved (15 configs)
{R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) : i.range = LieIdeal.toLieSubalgebra R L p.ker ↔ Function.Exact ⇑i ⇑p - mh_alge_1616b5AlgebrahardMathlib held-out✕ unsolved (15 configs)
{ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [_root_.Module K M] [Finite ι] [Infinite K] (f : ι → Module.Dual K M) (h : ∀ (i : ι), ∃ x, (f i) x ≠ 0) : ∃ x, ∀ (i : ι), (f i) x ≠ 0 - mh_alge_ccfab2AlgebraeasyMathlib held-out✕ unsolved (15 configs)
{R : Type u_1} {S : Type u_2} [SetLike S R] (s : S) [Semiring R] [PartialOrder R] [IsOrderedRing R] [SubsemiringClass S R] : IsOrderedRing ↥s - mh_alge_b01af0AlgebrahardMathlib held-out✕ unsolved (15 configs)
{α : Type u_5} [NonUnitalNonAssocCommSemiring α] (a : α) : a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (AddMonoid.End.mulLeft b) (AddMonoid.End.mulLeft a) - mh_alge_30a813AlgebrahardMathlib held-out✕ unsolved (15 configs)
{R : Type u_2} {a b : R} [CommRing R] {r : R} : (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R - mh_alge_458b8eAlgebramediumMathlib held-out✕ unsolved (15 configs)
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u₁ v, v, max (max (max u u₁) (v + 1)) v₁, max u (v + 1)} (PresheafOfModules.evaluation R X) - mh_alge_607566AlgebramediumMathlib held-out✕ unsolved (15 configs)
(K : Type u_7) {L : Type u_8} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (x : L) : Module.finrank K ↥(LieSubalgebra.engel K x) = (LinearMap.charpoly ((LieAlgebra.ad K L) x)).natTrailingDegree - mh_alge_17fd53AlgebraeasyMathlib held-out✓ solved by 5/15
{α : Type u_1} {n : ℕ} [DecidableEq α] [Fintype α] {m : ℕ} (hm : m + n = Fintype.card α) : Set.powersetCard.compl hm = Set.powersetCard.compl hm - mh_alge_740845AlgebraeasyMathlib held-out✕ unsolved (15 configs)
{R : Type u} [Ring R] : CategoryTheory.Limits.HasFiniteBiproducts (ModuleCat R) - mh_alge_8f6995AlgebrahardMathlib held-out✕ unsolved (15 configs)
{A : Type u_1} [AddMonoid A] [StarAddMonoid A] {r : A → A → Prop} (hr : ∀ (a b : A), r a b → r (star a) (star b)) ⦃a b : A⦄ : AddConGen.Rel r a b → AddConGen.Rel r (star a) (star b) - mh_alge_1a9c88AlgebraeasyMathlib held-out✕ unsolved (15 configs)
(G : Type u) [CommGroup G] [Group.FG G] (hG : IsMulTorsion G) : Finite G - mh_alge_8ed2b0AlgebraeasyMathlib held-out✕ unsolved (15 configs)
{α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [MOD n] - mh_alge_8025e5AlgebramediumMathlib held-out✕ unsolved (15 configs)
{K : Type u_1} {v : K} {n : ℕ} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {b : K} (nth_partDenom_eq : (GenContFract.of v).partDens.get? n = some b) : b * (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1) - mh_alge_2e2be9AlgebrahardMathlib held-out✕ unsolved (15 configs)
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {I : C} [CategoryTheory.Injective I] {L : CochainComplex C ℤ} {i : ℤ} (ι : (CochainComplex.singleFunctor C i).obj I ⟶ L) [L.IsStrictlyGE i] [QuasiIsoAt ι i] : CategoryTheory.IsSplitMono ι - mh_alge_692c04AlgebramediumMathlib held-out✓ solved by 8/15
(R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing A] [LieRing L] [_root_.Module A L] [LieRingModule L A] [LieRinehartRing A L] [CommRing R] [Algebra R A] [LieAlgebra R L] : LieRinehartAlgebra R A L = LieRinehartAlgebra R A L - mh_alge_ea4d0fAlgebrahardMathlib held-out✕ unsolved (15 configs)
(R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [LieAlgebra.IsKilling R L] : LieAlgebra.IsKilling R ↥(LieDerivation.ad R L).range - mh_alge_862f71AlgebrahardMathlib held-out✕ unsolved (15 configs)
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (HomotopyCategory.plus C).IsVerdierRightLocalizing (HomotopyCategory.subcategoryAcyclic C) - mh_alge_2bbbefAlgebraeasyMathlib held-out✓ solved by 2/15
{K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.nums 0 = g.h - mh_alge_2cc299AlgebrahardMathlib held-out✕ unsolved (15 configs)
: (CategoryTheory.forget₂ RingCat AddCommGrpCat).IsRightAdjoint - mh_alge_c1cd6dAlgebraeasyMathlib held-out · devnot attempted
{R : Type u_1} [Ring R] (M : ModuleCat R) [CategoryTheory.Simple M] : IsSimpleModule R ↑M - mh_alge_1c5663AlgebramediumMathlib held-out · devnot attempted
{α : Type u_1} {G₀ : Type u_2} [GroupWithZero G₀] [SMul α G₀] [SMulCommClass G₀ α G₀] [IsScalarTower α G₀ G₀] : SMulCommClass (ConjAct G₀) α G₀ - mh_alge_0b4529AlgebraeasyMathlib held-out · devnot attempted
{ι : Type u_1} {α : Type u_2} {R : ι → Type u_3} [(i : ι) → SMul α (R i)] {r : α} [∀ (i : ι), Nonempty (R i)] : IsSMulRegular ((i : ι) → R i) r ↔ ∀ (i : ι), IsSMulRegular (R i) r - mh_alge_d53ceaAlgebraeasyMathlib held-out · devnot attempted
{G : Type u} [Group G] [IsFreeGroup G] (H : Subgroup G) : IsFreeGroup ↥H - mh_alge_6b714eAlgebrahardMathlib held-out · devnot attempted
{R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] (i : σ) (p : MvPolynomial σ R) (n : ℕ) (hp : p ≠ 0) : MvPolynomial.degreeOf i (p ^ n) = n * MvPolynomial.degreeOf i p - novel_alg_01AlgebraeasyAuthored✓ solved by 9/15
(a b : ℝ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 - novel_alg_02AlgebramediumAuthored✓ solved by 1/15
(x : ℝ) (hx : x ≠ 1) : (x ^ 3 - 1) / (x - 1) = x ^ 2 + x + 1 - novel_alg_03AlgebraeasyAuthored✓ solved by 1/15
(a b c : ℚ) (h₁ : a + b = 5) (h₂ : b + c = 7) (h₃ : a + c = 6) : a = 2 - novel_alg_04AlgebramediumAuthored✓ solved by 1/15
(x y : ℝ) (h₁ : x + y = 10) (h₂ : x - y = 4) : x * y = 21 - novel_alg_05AlgebramediumAuthored✕ unsolved (15 configs)
(n : ℕ) : ∑ i ∈ Finset.range (n + 1), (2 * i + 1) = (n + 1) ^ 2 - novel_alg_06AlgebramediumAuthored✓ solved by 1/15
(x : ℝ) (h : x ^ 2 - 5 * x + 6 = 0) : x = 2 ∨ x = 3 - novel_alg_07AlgebramediumAuthored✕ unsolved (15 configs)
(f : ℕ → ℕ) (h0 : f 0 = 1) (hs : ∀ n, f (n + 1) = 2 * f n) (n : ℕ) : f n = 2 ^ n - novel_alg_08AlgebrahardAuthored✕ unsolved (15 configs)
(n : ℕ) : ∑ i ∈ Finset.range (n + 1), (i : ℚ) = n * (n + 1) / 2 - novel_alg_09AlgebramediumAuthored✓ solved by 3/15
(x : ℝ) (hx : 0 < x) : Real.log (x ^ 3) = 3 * Real.log x - novel_alg_10AlgebraeasyAuthored✓ solved by 2/15
{G : Type*} [Group G] (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ - novel_ineq_01InequalitieseasyAuthored✓ solved by 1/15
(a b : ℝ) : 2 * a * b ≤ a ^ 2 + b ^ 2 - novel_ineq_02InequalitiesmediumAuthored✕ unsolved (15 configs)
(x : ℝ) (hx : 0 < x) : x + 1 / x ≥ 2 - novel_ineq_03InequalitieseasyAuthored✕ unsolved (15 configs)
(a b c : ℝ) : a * b + b * c + c * a ≤ a ^ 2 + b ^ 2 + c ^ 2 - novel_ineq_04InequalitiesmediumAuthored✕ unsolved (15 configs)
(a b : ℝ) (ha : 0 < a) (hb : 0 < b) : (a + b) * (1 / a + 1 / b) ≥ 4 - novel_ineq_05InequalitieseasyAuthored✕ unsolved (15 configs)
(x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x + y = 2) : x * y ≤ 1 - novel_ineq_06InequalitieshardAuthored✕ unsolved (15 configs)
(a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b + b / c + c / a ≥ 3 - novel_ineq_07InequalitieseasyAuthored✓ solved by 9/15
(x : ℝ) : Real.cos x ^ 2 ≤ 1 - novel_ineq_08InequalitieseasyAuthored✓ solved by 1/15
(n : ℕ) (hn : 3 ≤ n) : n ^ 2 ≥ 2 * n + 3 - novel_ineq_09InequalitiesmediumAuthored✕ unsolved (15 configs)
(n : ℕ) (hn : 1 ≤ n) : n + 1 ≤ 2 ^ n - novel_ineq_10InequalitieseasyAuthored✕ unsolved (15 configs)
(p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) : p * (1 - p) ≤ 1 / 4 - novel_nt_01Number theoryhardAuthored✕ unsolved (15 configs)
(n : ℕ) : 6 ∣ n * (n + 1) * (n + 2) - novel_nt_02Number theorymediumAuthored✕ unsolved (15 configs)
(n : ℕ) : Nat.gcd (2 * n + 1) (n + 1) = 1 - novel_nt_03Number theoryeasyAuthored✓ solved by 8/15
(p : ℕ) (hp : p.Prime) (h2 : p ≠ 2) : Odd p - novel_nt_04Number theoryeasyAuthored✕ unsolved (15 configs)
(x : ℤ) (h : 3 ∣ x) : 9 ∣ x ^ 2 - novel_nt_05Number theorymediumAuthored✕ unsolved (15 configs)
(n : ℕ) : (n ^ 2 + n) % 2 = 0 - novel_nt_06Number theoryhardAuthored✕ unsolved (15 configs)
(n : ℕ) : ¬ 3 ∣ n ^ 2 + 1 - novel_nt_07Number theorymediumAuthored✓ solved by 6/15
(a b : ℤ) (h : a ≡ b [ZMOD 5]) : a ^ 2 ≡ b ^ 2 [ZMOD 5] - novel_nt_08Number theoryhardAuthored✓ solved by 1/15
(a b : ℕ) (h : a * b = 12) (ha : a > b) (hb : b > 2) : a = 4 - novel_nt_09Number theoryeasyAuthored✕ unsolved (15 configs)
(a : ℤ) : a ^ 2 % 4 = 0 ∨ a ^ 2 % 4 = 1 - novel_nt_10Number theoryeasyAuthored✓ solved by 7/15
: Nat.choose 10 3 = 120 - novel_set_01SetseasyAuthored✓ solved by 2/15
{α : Type*} (A B C : Set α) : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) - novel_set_02SetseasyAuthored✓ solved by 1/15
{α : Type*} (A B : Set α) (h : A ⊆ B) : A ∪ B = B - novel_set_03SetsmediumAuthored✓ solved by 1/15
{α : Type*} (A B C : Set α) (h₁ : A ⊆ B) (h₂ : B ⊆ C) : A \ C = ∅ - novel_set_04SetseasyAuthored✓ solved by 5/15
{α : Type*} (A B : Set α) : (A ∪ B)ᶜ = Aᶜ ∩ Bᶜ - novel_set_05SetsmediumAuthored✓ solved by 1/15
{α : Type*} (s : Set α) (f : α → α) (hf : ∀ x, f (f x) = x) : f '' (f '' s) = s - novel_set_06SetseasyAuthored✓ solved by 1/15
(S : Set ℕ) (hS : S = {n | n % 2 = 0}) : 4 ∈ S ∧ 3 ∉ S - novel_set_07SetsmediumAuthored✓ solved by 1/15
: (Finset.filter (fun n => n % 3 = 0) (Finset.range 30)).card = 10 - novel_set_08SetsmediumAuthored✓ solved by 1/15
{α : Type*} (A B : Set α) : A ⊆ B ↔ A ∩ B = A - novel_fun_01FunctionseasyAuthored✓ solved by 6/15
{α β γ : Type*} (f : α → β) (g : β → γ) (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (g ∘ f) - novel_fun_02FunctionseasyAuthored✓ solved by 1/15
{α β : Type*} (f : α → β) (g : β → α) (h : ∀ x, g (f x) = x) : Function.Injective f - novel_fun_03FunctionseasyAuthored✕ unsolved (15 configs)
(f : ℝ → ℝ) (hf : ∀ x, f x = 3 * x + 2) : Function.Injective f - novel_fun_04FunctionsmediumAuthored✕ unsolved (15 configs)
(f : ℝ → ℝ) (hf : ∀ x y, f (x + y) = f x + f y) : f 0 = 0 - novel_fun_05FunctionsmediumAuthored✓ solved by 1/15
(f : ℕ → ℕ) (hf : StrictMono f) (n : ℕ) : n ≤ f n - novel_fun_06FunctionshardAuthored✕ unsolved (15 configs)
(f : ℝ → ℝ) (hf : ∀ x y, f (x + y) = f x + f y) (x : ℝ) : f (-x) = -f x - novel_fun_07FunctionsmediumAuthored✓ solved by 1/15
{α β : Type*} (f : α → β) (hf : Function.Surjective f) (g h : β → α) (hg : g ∘ f = h ∘ f) : g = h - novel_prob_01ProbabilitymediumAuthored✓ solved by 1/15
(p : NNReal) (h : p ≤ 1) : PMF.bernoulli p h true = (p : ENNReal) - novel_prob_02ProbabilityeasyAuthored✓ solved by 1/15
{Ω : Type*} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (s : Set Ω) : μ s ≤ 1 - novel_prob_03ProbabilitymediumAuthored✓ solved by 1/15
{Ω : Type*} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (A : Set Ω) (hA : MeasurableSet A) : μ Aᶜ = 1 - μ A - novel_prob_04ProbabilitymediumAuthored✓ solved by 9/15
(n : ℕ) : ∑ k ∈ Finset.range (n + 1), Nat.choose n k = 2 ^ n - novel_cat_01Category theoryeasyAuthored✓ solved by 10/15
{C : Type*} [Category C] {X Y : C} (α : X ≅ Y) : α.hom ≫ α.inv = 𝟙 X - novel_cat_02Category theorymediumAuthored✓ solved by 1/15
{C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [IsIso g] : IsIso (f ≫ g) - novel_cat_03Category theorymediumAuthored✓ solved by 1/15
{C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) [Mono f] (g h : Z ⟶ X) (w : g ≫ f = h ≫ f) : g = h - novel_cat_04Category theoryhardAuthored✓ solved by 1/15
{C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono f] [Mono g] : Mono (f ≫ g)