---

Margulis, G. A., Indefinite quadratic forms and unipotent flows on homogeneous spaces, Banach Center Publ. 23 (1989), 399–409, Theorem 1, and Discrete subgroups and ergodic theory, in Number theory, trace formulas and discrete groups (Oslo, 1987), Academic Press (1989), 377–398, the chapter the site cites as [Ma89]. The theorem, Oppenheim's conjecture: a real nondegenerate indefinite quadratic form in at least three variables that is not a multiple of a rational form takes values of arbitrarily small absolute value at nonzero integer vectors. Applied to $Q(X,Y,Z)=X^2+Y^2-\alpha Z^2$ with $\alpha>0$ irrational, which is nondegenerate, indefinite and not proportional to a rational form, it gives for every $\epsilon>0$ an integer vector $(a,b,c)\ne0$ with $|Q(a,b,c)|<\epsilon$.

With tolerance $\delta=\min\{1,\alpha,\epsilon/25\}$ in place of $\epsilon$, the vector has $c\ne0$ and $(a,b)\ne(0,0)$, and $(|a|,|b|,|c|)$, or $(3t,4t,5|c|)$ when one of $a,b$ vanishes and $t$ is the other's absolute value, gives positive integers $x,y,z$ with $|x^2+y^2-z^2\alpha|<25\delta\le\epsilon$. For every positive irrational $\alpha$ this is the corrected Statement of Problem 496. The passage is written out on the companion page of the source card; that deduction is this corpus's and has had no outside review. The companion also notes that the value cannot be zero, since $\alpha$ is irrational.

Acceptance. Reviewed: the erdosproblems.com page for Problem 496 (accessed 2026-10-07) is labeled proved by the site's curator, Thomas Bloom, who writes that the statement is true and was proved by Margulis [Ma89]; that acceptance reads the problem for positive $\alpha$, the setting of Oppenheim's conjecture that Erdős's 1961 question (source page) came from and the setting of the corrected Statement. The theorem is published in the two venues above; this corpus has not established their refereeing and lists no refereed evidence. The Banach Center paper's statement (p. 399) and its reduction to its Theorem 2 (p. 400) are transcribed on the companion page; its homogeneous-dynamics proof is not reconstructed in this repository, which awards no tier of its own.

Formalization. The Lean development Erdos496.lean in Boris Alexeev's repository, added on 2026-08-21 and linked above at a pinned commit, written by Codex and GPT-5.6 Sol with Margulis named as informal author, proves erdos_496_positive: the conclusion for every irrational $\alpha>0$, taking as an explicit hypothesis the specialization of the Oppenheim–Margulis theorem to the form $a^2+b^2-\alpha c^2$ (small nonzero values at nonzero integer vectors) and supplying the same positive-coordinate transfer as the companion page, through the $3$-$4$-$5$ rotation. The theorem is conditional on Margulis's theorem, which it does not prove. The same file's disproof of the site's wording has [[problems/irrationality/E0496/claims/2026_08_21_alexeev|its own page]], rejected because it answers the site's wording, not the corrected statement. The hypothesis is no stronger than Theorem 1: its nonzero-value clause holds automatically, since a zero value at a nonzero integer vector would make $\alpha$ rational. It is still unformalized, and it is the whole depth of the claim, so a build checks only the coordinate transfer. This corpus's verification built the file at the pinned commit (Lean v4.33.0, Mathlib v4.33.0): erdos_496_positive depends only on the axioms propext, Classical.choice and Quot.sound, and its statement matches the file's comparator challenge. formalized does not apply to this claim, since the build leaves Margulis's theorem assumed.

Depends on. Nothing in this wiki; the claim rests on the cited theorem.