The 290 theorem

two_ninety_theorem

Submitter: Bolton Bailey/Project Numina.

Notes: The 290 theorem (Bhargava–Hanke): a positive-definite integral quadratic form represents every positive integer if it represents a particular collection of 29 critical numbers below 290.

Source: M. Bhargava, J. Hanke, Universal quadratic forms and the 290-theorem, preprint (2011). See also https://en.wikipedia.org/wiki/15_and_290_theorems

Informal solution: The proof combines advances in the escalation method and bounds on Fourier coefficients of weight 2 theta functions. It also uses a trick to allow the analysis to focus mainly on quaternary forms.

theorem declaration uses `sorry`two_ninety_theorem {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
    (hpos : M.PosDef)
    (hIntegral : LeanEval.NumberTheory.TwoNinety.Integral M)
    (hrep : ∀ m ∈ LeanEval.NumberTheory.TwoNinety.criticalNumbers, LeanEval.NumberTheory.TwoNinety.Represents M m) :
    LeanEval.NumberTheory.TwoNinety.IsUniversal M := byn:ℕM:Matrix (Fin n) (Fin n) ℝhpos:M.PosDefhIntegral:Integral Mhrep:∀ m ∈ criticalNumbers, LeanEval.NumberTheory.TwoNinety.Represents M m⊢ IsUniversal M
  sorryAll goals completed! 🐙

Solved by

Not yet solved.