Lorentzian polynomials | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: P. Brändén and J. Huh, `Lorentzian polynomials`, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-3-LorentzianPolynomials.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_2_25 (n d : ℕ) (hn : 0 < n) : closure (Ŀ n d) = LorentzianPolynomials.L n d := byn:ℕd:ℕhn:0 < n⊢ closure (Ŀ n d) = L n d
  sorryAll goals completed! 🐙