def Oppenheim.IsIndefinite {n : ℕ} (Q : QuadraticForm ℝ (Fin n → ℝ)) : Prop

A real quadratic form $Q$ is indefinite if it has mixed signature, i.e. it attains both strictly positive and strictly negative values.

def Oppenheim.IsProportionalToIntegerForm {n : ℕ} (Q : QuadraticForm ℝ (Fin n → ℝ)) : Prop

A real quadratic form $Q$ is proportional to an integer form if there exist a scalar $c \in \mathbb{R}$ and an integer matrix $M$ such that the Gram matrix of $Q$ equals $c \cdot M$ (i.e. the coefficients of $Q$ all lie in $\mathbb{Z}\alpha$ for some $\alpha$).

theorem Oppenheim.oppenheim_conjecture {n : ℕ} (hn : n ≥ 3) (Q : QuadraticForm ℝ (Fin n → ℝ)) (hnd : QuadraticMap.Nondegenerate) (hind : IsIndefinite Q) (hrat : ¬IsProportionalToIntegerForm Q) : Dense (Set.range fun (v : Fin n → ℤ) => Q fun (i : Fin n) => ↑(v i))

Oppenheim conjecture (Margulis): if $n \ge 3$, $Q$ is a nondegenerate indefinite real quadratic form in $n$ variables whose coefficients are not all proportional to integers, then the set of values $Q(\mathbb{Z}^n)$ is dense in $\mathbb{R}$.