FormalConjectures.Paper.CasasAlvero

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil

Casas-Alvero Conjecture

References:

The Casas-Alvero conjecture for infinitely many degrees

MathOverflow

The Casas-Alvero conjecture states that if a univariate polynomial P of degree d over a field of characteristic zero shares a non-trivial factor with its Hasse derivatives up to order d-1, then P must be of the form (X - α)ᵈ for some α in the field.

The conjecture has been proven for:

Degrees d ≤ 8

Degrees of the form p^k where p is prime

Degrees of the form 2p^k where p is prime

The conjecture is false in positive characteristic p for polynomials of degree p+1.

The conjecture is now claimed to be proven in this paper:

Proof of the Casas-Alvero conjecture: Soham Ghosh)


namespace CasasAlvero


open Polynomial


variable {K L : Type*} [Field K] [Field L] {f : K →+* L}

A polynomial P satisfies the Casas-Alvero property if it shares a factor with each of its Hasse derivatives up to order d-1, where d is the degree of P.

def HasCasasAlveroProp (P : K[X]) : Prop :=
  ∀ i ∈ Finset.range P.natDegree, ¬ IsCoprime P (P.hasseDeriv i)

A stronger version of the Casas-Alvero property, which requires that the polynomial P shares a root with each of its Hasse derivatives up to order deg P - 1. The subscript r indicates "root" in the definition.


def HasCasasAlveroPropᵣ (P : K[X]) : Prop :=
  ∀ i ∈ Finset.range P.natDegree, ∃ α : K, IsRoot P α ∧ IsRoot (P.hasseDeriv i) α


@[category API, AMS 12]
theorem HasCasasAlveroPropᵣ.hasCasasAlveroProp {P : K[X]}
    (hca : HasCasasAlveroPropᵣ P) : HasCasasAlveroProp P := byK:Type u_1inst✝:Field KP:K[X]hca:HasCasasAlveroPropᵣ P⊢ HasCasasAlveroProp P
  intro i hiK:Type u_1inst✝:Field KP:K[X]hca:HasCasasAlveroPropᵣ Pi:ℕhi:i ∈ Finset.range P.natDegree⊢ ¬IsCoprime P ((hasseDeriv i) P) coprimeK:Type u_1inst✝:Field KP:K[X]hca:HasCasasAlveroPropᵣ Pi:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)⊢ False
  simp_rw [K:Type u_1inst✝:Field KP:K[X]hca:HasCasasAlveroPropᵣ Pi:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)⊢ FalseHasCasasAlveroPropᵣ, ← dvd_iff_isRoot] at hca
  have ⟨α, hα, hαi⟩ := hca i hiK:Type u_1inst✝:Field KP:K[X]i:ℕhi:i ∈ Finset.range P.natDegreecoprime:IsCoprime P ((hasseDeriv i) P)hca:∀ i ∈ Finset.range P.natDegree, ∃ α, X - C α ∣ P ∧ X - C α ∣ (hasseDeriv i) Pα:Khα:X - C α ∣ Phαi:X - C α ∣ (hasseDeriv i) P⊢ False
  exact not_isUnit_X_sub_C _ (coprime.isUnit_of_dvd' hα hαi)All goals completed! 🐙


@[category API, AMS 12]
theorem HasCasasAlveroProp.map_iff {P : K[X]} :
    HasCasasAlveroProp (P.map f) ↔ HasCasasAlveroProp P := byK:Type u_1L:Type u_2inst✝¹:Field Kinst✝:Field Lf:K →+* LP:K[X]⊢ HasCasasAlveroProp (map f P) ↔ HasCasasAlveroProp P
  simp_rw [K:Type u_1L:Type u_2inst✝¹:Field Kinst✝:Field Lf:K →+* LP:K[X]⊢ HasCasasAlveroProp (map f P) ↔ HasCasasAlveroProp PHasCasasAlveroProp]
  congr!a.h.h.h.e'_4.h.e'_1K:Type u_1L:Type u_2inst✝¹:Field Kinst✝:Field Lf:K →+* LP:K[X]a✝:ℕ⊢ (map f P).natDegree = P.natDegreea.h.h'.h.e'_1.aK:Type u_1L:Type u_2inst✝¹:Field Kinst✝:Field Lf:K →+* LP:K[X]a✝¹:ℕa✝:a✝¹ ∈ Finset.range P.natDegree⊢ IsCoprime (map f P) ((hasseDeriv a✝¹) (map f P)) ↔ IsCoprime P ((hasseDeriv a✝¹) P)
  ·a.h.h.h.e'_4.h.e'_1K:Type u_1L:Type u_2inst✝¹:Field Kinst✝:Field Lf:K →+* LP:K[X]a✝:ℕ⊢ (map f P).natDegree = P.natDegree exact natDegree_map _All goals completed! 🐙
  ·a.h.h'.h.e'_1.aK:Type u_1L:Type u_2inst✝¹:Field Kinst✝:Field Lf:K →+* LP:K[X]a✝¹:ℕa✝:a✝¹ ∈ Finset.range P.natDegree⊢ IsCoprime (map f P) ((hasseDeriv a✝¹) (map f P)) ↔ IsCoprime P ((hasseDeriv a✝¹) P) rw [hasseDeriv_map, isCoprime_map]All goals completed! 🐙


@[category API, AMS 12]
theorem hasCasasAlveroProp_iffᵣ {P : K[X]} [IsAlgClosed K] :
    HasCasasAlveroProp P ↔ HasCasasAlveroPropᵣ P := byK:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ HasCasasAlveroProp P ↔ HasCasasAlveroPropᵣ P
  refine ⟨?_, HasCasasAlveroPropᵣ.hasCasasAlveroProp⟩K:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ HasCasasAlveroProp P → HasCasasAlveroPropᵣ P
  simp_rw [K:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ HasCasasAlveroProp P → HasCasasAlveroPropᵣ PHasCasasAlveroProp, HasCasasAlveroPropᵣ,
    isCoprime_iff_aeval_ne_zero_of_isAlgClosed K K, coe_aeval_eq_eval]
  push_negK:Type u_1inst✝¹:Field KP:K[X]inst✝:IsAlgClosed K⊢ (∀ i ∈ Finset.range P.natDegree, ∃ a, eval a P = 0 ∧ eval a ((hasseDeriv i) P) = 0) →
  ∀ i ∈ Finset.range P.natDegree, ∃ α, P.IsRoot α ∧ ((hasseDeriv i) P).IsRoot α
  exact (· · ·)All goals completed! 🐙


universe u in

Note that whether we use HasCasasAlveroProp or HasCasasAlveroPropᵣ to state the Casas-Alvero conjecture, we obtain the following equivalent statements.

@[category API, AMS 12]
lemma casas_alvero_iffᵣ :
    (∀ {K : Type u} [Field K] [CharZero K] (P : K[X]),
      P.Monic → HasCasasAlveroProp P → ∃ α : K, P = (X - C α) ^ P.natDegree) ↔
    (∀ {K : Type u} [Field K] [CharZero K] (P : K[X]),
      P.Monic → HasCasasAlveroPropᵣ P → ∃ α : K, P = (X - C α) ^ P.natDegree) := by⊢ (∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroProp P → ∃ α, P = (X - C α) ^ P.natDegree) ↔
  ∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegree
  refine ⟨fun h _ _ _ P hP hca ↦ h P hP hca.hasCasasAlveroProp, fun h K _ _ P hP hca ↦ ?_⟩h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  let L := AlgebraicClosure Kh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure K⊢ ∃ α, P = (X - C α) ^ P.natDegree
  have ⟨α, eq⟩ := h (P.map (algebraMap K L)) (hP.map _) <|
    hasCasasAlveroProp_iffᵣ.mp <| HasCasasAlveroProp.map_iff.mpr hcah:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegree⊢ ∃ α, P = (X - C α) ^ P.natDegree
  by_cases h0 : P.natDegree = 0posh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:P.natDegree = 0⊢ ∃ α, P = (X - C α) ^ P.natDegreenegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0⊢ ∃ α, P = (X - C α) ^ P.natDegree
  ·posh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:P.natDegree = 0⊢ ∃ α, P = (X - C α) ^ P.natDegree simp [hP.natDegree_eq_zero.mp h0]All goals completed! 🐙
  let α' := - P.nextCoeff / P.natDegreenegh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ ∃ α, P = (X - C α) ^ P.natDegree
  have : algebraMap K L α' = α := by⊢ (∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroProp P → ∃ α, P = (X - C α) ^ P.natDegree) ↔
  ∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
    P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegree
    simp_rw [h:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegree⊢ (algebraMap K L) α' = αα', div_eq_inv_mul, map_mul, map_neg, ← nextCoeff_map (algebraMap K L).injective,
      congr_arg nextCoeff eq, (monic_X_sub_C α).nextCoeff_pow, nextCoeff_X_sub_C, nsmul_eq_mul,
      mul_neg _ α, neg_neg, ← mul_assoc, natDegree_map, map_inv₀, map_natCast]
    rw [inv_mul_cancel₀ (Nat.cast_ne_zero.mpr h0), one_mul]All goals completed! 🐙
  use α'hh:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α := 
  id
    (Eq.mpr (id (congrArg (fun x => (algebraMap K L) x = α) (div_eq_inv_mul (-P.nextCoeff) ↑P.natDegree)))
      (Eq.mpr (id (congrArg (fun x => x = α) (map_mul (algebraMap K L) (↑P.natDegree)⁻¹ (-P.nextCoeff))))
        (Eq.mpr
          (id (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * x = α) (map_neg (algebraMap K L) P.nextCoeff)))
          (Eq.mpr
            (id
              (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                ((fun p => Eq.symm (nextCoeff_map (RingHom.injective (algebraMap K L)) p)) P)))
            (Eq.mpr (id (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α) (congr_arg nextCoeff eq)))
              (Eq.mpr
                (id
                  (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                    ((fun n => Monic.nextCoeff_pow (monic_X_sub_C α) n) (map (algebraMap K L) P).natDegree)))
                (Eq.mpr
                  (id
                    (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -((map (algebraMap K L) P).natDegree • x) = α)
                      (nextCoeff_X_sub_C α)))
                  (Eq.mpr
                    (id
                      (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                        (nsmul_eq_mul (map (algebraMap K L) P).natDegree (-α))))
                    (Eq.mpr
                      (id
                        (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                          ((fun x_0 => (fun x_0 => mul_neg x_0 α) x_0) ↑(map (algebraMap K L) P).natDegree)))
                      (Eq.mpr
                        (id
                          (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * x = α)
                            (neg_neg (↑(map (algebraMap K L) P).natDegree * α))))
                        (Eq.mpr
                          (id
                            (congrArg (fun x => x = α)
                              (casas_alvero_iffᵣ._simp_1 ((algebraMap K L) (↑P.natDegree)⁻¹)
                                (↑(map (algebraMap K L) P).natDegree) α)))
                          (Eq.mpr
                            (id
                              (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * ↑x * α = α)
                                (natDegree_map (algebraMap K L))))
                            (Eq.mpr
                              (id (congrArg (fun x => x * ↑P.natDegree * α = α) (map_inv₀ (algebraMap K L) ↑P.natDegree)))
                              (Eq.mpr
                                (id
                                  (congrArg (fun x => x⁻¹ * ↑P.natDegree * α = α)
                                    (map_natCast (algebraMap K L) P.natDegree)))
                                (Eq.mpr (id (congrArg (fun _a => _a * α = α) (inv_mul_cancel₀ (Nat.cast_ne_zero.mpr h0))))
                                  (Eq.mpr (id (congrArg (fun _a => _a = α) (one_mul α))) (Eq.refl α)))))))))))))))))⊢ P = (X - C α') ^ P.natDegree
  apply map_injective _ (algebraMap K L).injectiveh.ah:∀ {K : Type u} [inst : Field K] [CharZero K] (P : K[X]),
  P.Monic → HasCasasAlveroPropᵣ P → ∃ α, P = (X - C α) ^ P.natDegreeK:Type ux✝¹:Field Kx✝:CharZero KP:K[X]hP:P.Monichca:HasCasasAlveroProp PL:Type u := AlgebraicClosure Kα:Leq:map (algebraMap K L) P = (X - C α) ^ (map (algebraMap K L) P).natDegreeh0:¬P.natDegree = 0α':K := -P.nextCoeff / ↑P.natDegreethis:(algebraMap K L) α' = α := 
  id
    (Eq.mpr (id (congrArg (fun x => (algebraMap K L) x = α) (div_eq_inv_mul (-P.nextCoeff) ↑P.natDegree)))
      (Eq.mpr (id (congrArg (fun x => x = α) (map_mul (algebraMap K L) (↑P.natDegree)⁻¹ (-P.nextCoeff))))
        (Eq.mpr
          (id (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * x = α) (map_neg (algebraMap K L) P.nextCoeff)))
          (Eq.mpr
            (id
              (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                ((fun p => Eq.symm (nextCoeff_map (RingHom.injective (algebraMap K L)) p)) P)))
            (Eq.mpr (id (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α) (congr_arg nextCoeff eq)))
              (Eq.mpr
                (id
                  (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                    ((fun n => Monic.nextCoeff_pow (monic_X_sub_C α) n) (map (algebraMap K L) P).natDegree)))
                (Eq.mpr
                  (id
                    (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -((map (algebraMap K L) P).natDegree • x) = α)
                      (nextCoeff_X_sub_C α)))
                  (Eq.mpr
                    (id
                      (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                        (nsmul_eq_mul (map (algebraMap K L) P).natDegree (-α))))
                    (Eq.mpr
                      (id
                        (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * -x = α)
                          ((fun x_0 => (fun x_0 => mul_neg x_0 α) x_0) ↑(map (algebraMap K L) P).natDegree)))
                      (Eq.mpr
                        (id
                          (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * x = α)
                            (neg_neg (↑(map (algebraMap K L) P).natDegree * α))))
                        (Eq.mpr
                          (id
                            (congrArg (fun x => x = α)
                              (casas_alvero_iffᵣ._simp_1 ((algebraMap K L) (↑P.natDegree)⁻¹)
                                (↑(map (algebraMap K L) P).natDegree) α)))
                          (Eq.mpr
                            (id
                              (congrArg (fun x => (algebraMap K L) (↑P.natDegree)⁻¹ * ↑x * α = α)
                                (natDegree_map (algebraMap K L))))
                            (Eq.mpr
                              (id (congrArg (fun x => x * ↑P.natDegree * α = α) (map_inv₀ (algebraMap K L) ↑P.natDegree)))
                              (Eq.mpr
                                (id
                                  (congrArg (fun x => x⁻¹ * ↑P.natDegree * α = α)
                                    (map_natCast (algebraMap K L) P.natDegree)))
                                (Eq.mpr (id (congrArg (fun _a => _a * α = α) (inv_mul_cancel₀ (Nat.cast_ne_zero.mpr h0))))
                                  (Eq.mpr (id (congrArg (fun _a => _a = α) (one_mul α))) (Eq.refl α)))))))))))))))))⊢ map (algebraMap K L) P = map (algebraMap K L) ((X - C α') ^ P.natDegree)
  simpa [this] using eqAll goals completed! 🐙


section conjecture


variable [CharZero K] (P : K[X]) (hP : Monic P)

include hP

The Casas-Alvero conjecture states that in characteristic zero, if a monic polynomial P has the Casas-Alvero property, then P = (X - α)ᵈ for some α.

@[category research open, AMS 12]
theorem declaration uses 'sorry'casas_alvero_conjecture (hP' : HasCasasAlveroProp P) :
    ∃ α : K, P = (X - C α) ^ P.natDegree := byK:Type u_1inst✝¹:Field Kinst✝:CharZero KP:K[X]hP:P.MonichP':HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙

The Casas-Alvero conjecture holds for polynomials of prime power degree. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

@[category research solved, AMS 12]
theorem declaration uses 'sorry'casas_alvero.prime_power (p k : ℕ) (hp : p.Prime) (hd : P.natDegree = p^k)
    (hP' : HasCasasAlveroProp P) : ∃ α : K, P = (X - C α) ^ P.natDegree := byK:Type u_1inst✝¹:Field Kinst✝:CharZero KP:K[X]hP:P.Monicp:ℕk:ℕhp:Nat.Prime phd:P.natDegree = p ^ khP':HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙

The Casas-Alvero conjecture holds for polynomials of degree 2p^k where p is prime. This was proved by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

@[category research solved, AMS 12]
theorem declaration uses 'sorry'casas_alvero.double_prime_power (p k : ℕ) (hp : p.Prime) (hd : P.natDegree = 2 * p^k)
    (hP' : HasCasasAlveroProp P) : ∃ α : K, P = (X - C α) ^ P.natDegree := byK:Type u_1inst✝¹:Field Kinst✝:CharZero KP:K[X]hP:P.Monicp:ℕk:ℕhp:Nat.Prime phd:P.natDegree = 2 * p ^ khP':HasCasasAlveroProp P⊢ ∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙


end conjecture

The Casas-Alvero conjecture fails in positive characteristic p for polynomials of degree p + 1. This was shown by Graf von Bothmer, Labs, Schicho, and van de Woestijne.

Reference: The Casas-Alvero conjecture for infinitely many degrees

Formal proof linked here provided by AlphaProof.

@[category research solved, AMS 12, formal_proof using formal_conjectures at "https://github.com/mzhorvath1/formal-conjectures/blob/4f2343508f2c157f35abb7be4814bd550280ce81/FormalConjectures/Paper/CasasAlvero.lean#163"]
theorem declaration uses 'sorry'casas_alvero.positive_char_counterexample {p : ℕ} (hp : p.Prime) :
    ∃ (K : Type*) (_ : Field K) (_ : CharP K p),
      let P := X ^ (p + 1) - X ^ p
      Monic P ∧ HasCasasAlveroProp P ∧
      ¬∃ α : K, P = (X - C α) ^ P.natDegree := byp:ℕhp:Nat.Prime p⊢ ∃ K x,
  ∃ (_ : CharP K p),
    let P := X ^ (p + 1) - X ^ p;
    P.Monic ∧ HasCasasAlveroProp P ∧ ¬∃ α, P = (X - C α) ^ P.natDegree
  sorryAll goals completed! 🐙


end CasasAlvero