Wilkie's conjecture for Pfaffian structures | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: G. Binyamini, D. Novikov, and B. Zak, `Wilkie's conjecture for Pfaffian structures`, Annals of Math, 199 (2) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-199-2-WilkiesConjecture.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`corollary_1 (X : Set ℝⁿ) (h : WilkiesConjecture.IsRExpDefinable X) :
    ∃ f : MvPolynomial (Fin 2) ℝ, ∀ (g H : ℕ),
      Nat.card (WilkiesConjecture.degreeHeightLE X.trans g H) ≤ f.eval ![(g : ℝ), Real.log H] := byn:ℕX:Set (Fin n → ℝ)h:IsRExpDefinable X⊢ ∃ f, ∀ (g H : ℕ), ↑(Nat.card ↑(degreeHeightLE X.trans g H)) ≤ (MvPolynomial.eval ![↑g, Real.log ↑H]) f
  sorryAll goals completed! 🐙