A negative answer to Ulam's Problem 19 from the Scottish Book

Problem statement

Notes: Unavailable.

Source: D. Ryabogin, `A negative answer to Ulam's Problem 19 from the Scottish Book`, Annals of Math, 195 (3) 2022. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2022-195-3-Ulam.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1 (hd : 3 ≤ d) : letI : NeZero d := ⟨byd:ℕhd:3 ≤ d⊢ d ≠ 0 omegaAll goals completed! 🐙⟩
    ∃ K : Ulam.BodyOfRevolution d, Ulam.IsStrictlyConvexBody K.body ∧ ¬ Ulam.IsCentrallySymmetric K.body ∧
      Ulam.FloatsInEquilibriumInEveryOrientationAtLevel K.body (volume.real K.body / 2) := byd:ℕhd:3 ≤ d⊢ ∃ K,
  IsStrictlyConvexBody K.body ∧
    ¬IsCentrallySymmetric K.body ∧ FloatsInEquilibriumInEveryOrientationAtLevel K.body (volume.real K.body / 2)
  sorryAll goals completed! 🐙