---

Claim. The site's wording of Problem 496, over every irrational real $\alpha$, is false: for $\alpha=-\sqrt2$ and $\epsilon=1$ there are no positive integers $x,y,z$ with $|x^2+y^2-z^2\alpha|<1$, since the quantity equals $x^2+y^2+\sqrt2\,z^2\ge2$. The proof is the Lean development Erdos496.lean in Boris Alexeev's repository of formalized Erdős problems, added on 2026-08-21 and linked above at a pinned commit (Lean v4.33.0, Mathlib v4.33.0). Its theorem not_erdos_496 states the negation of the universal statement, with HasApproximation α ε encoding the existence of three positive integers within $\epsilon$; the file contains no sorry and prints the axioms of both of its theorems. The development's header names Grigory Margulis as informal author and Codex and GPT-5.6 Sol as formal authors.

The same file proves erdos_496_positive: for every irrational $\alpha>0$ the conclusion holds, with the specialization of the Oppenheim–Margulis theorem to the form $a^2+b^2-\alpha c^2$ (small nonzero values at nonzero integer vectors) taken as an explicit hypothesis (no stronger than Margulis's Theorem 1, since the value cannot vanish at a nonzero integer vector for irrational $\alpha$), and with the passage from a nonzero integer vector to three positive coordinates through the $3$-$4$-$5$ rotation. That theorem is the positive-parameter transfer recorded on [[problems/irrationality/E0496/claims/1989_01_01_margulis|Margulis's accepted full claim page]], which links the file as its formalization; it is not part of this claim.

Why it is rejected. The claim answers the site's wording, not the corrected statement. The corrected Statement of Problem 496 takes $\alpha>0$, the indefinite setting of Oppenheim's conjecture that the site names and that Margulis states, and the theorem settles no instance of it: every counterexample it gives has $\alpha<0$, where the form is positive definite. The problem page's Notes credit the disproof.

Standing. Rejected. Margulis never published the disproof of the site's wording, and the file's informal-author line credits Margulis only for the theorem behind the positive case, so the disproof is recorded as the repository's own result. The site (accessed 2026-09-04 and 2026-10-07) labels the problem PROVED, lists no proof claim and does not mention the development; the community database lists the problem as unformalized. No outside reviewer has examined the file. This corpus's verification built it at the pinned commit: not_erdos_496 depends only on the axioms propext, Classical.choice and Quot.sound, and its statement matches the file's comparator challenge. The build confirms the disproof of the site's wording and leaves the rejection unchanged, since the rejection concerns what the theorem answers.

Depends on. No page of this wiki.