Browning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literature
Random hypersurfaces with coefficients drawn uniformly from plus and minus one are shown to be smooth with probability tending to one as the degree grows, with a quantitative rate.
- Lab
- Axiom Math
- Model
- AxiomProver
- Field
- Mathematics
- Date
- 2026-09-16
- Human collaborators
- Ken Ono, Ashvin Swaminathan
- Problem posed
- 2025 · open 1 yr
What was found
Browning and Sawin conjectured that random hypersurfaces with sign coefficients are smooth with probability tending to one as the degree grows. The paper proves this and adds a rate: for each n at least 1, a degree d form in n+1 variables with independent uniform coefficients in plus and minus one defines a singular complex hypersurface with probability O_n(d^{-1/2}). Positive-dimensional singular loci are shown to occur with exponentially small probability, and for n at least 3 the same exponential bound is given for failure of absolute irreducibility. The abstract's AI disclosure is one sentence and covers the formalization: these results have been formalized in Lean by AxiomProver assuming existing literature.
Novelty check
The conjecture is attributed in the abstract to Browning and Sawin, whose 2025 preprint arXiv:2510.26191 is its source, and the 2026-09-23 watch run searched arXiv and the web for a prior proof and found none, making this the first claimed resolution. MathSciNet and Zentralblatt were not searched, and whether Browning or Sawin have themselves circulated a proof was not established.
Caveats and known objections
Autonomy is ai-assisted rather than stronger because the only AI role the abstract states is the Lean formalization. A separate and fuller disclosure describing human-AI collaboration through literature search, numerical experimentation and the proposal and rejection of candidate strategies was reported by the 2026-09-21 watch run as coming from this paper, but it does not appear in the abstract that was read directly on 2026-09-22; it may sit in the body. Until someone locates it, the autonomy grade here rests only on the formalization sentence, and a maintainer who finds that fuller text may have grounds to revisit it. Verification is claimed rather than formal because the formalization is explicitly conditional on existing literature taken as input, so the kernel certifies an implication; whether the five classical results taken as Lean axioms are standard or are doing substantive proof work is unresolved. A preprint days old at entry, unrefereed, with no specialist review and no discussion found on any tracked venue as of 2026-09-22.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-assisted.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-assisted for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Browning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literature. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-16-browning-sawin-hypersurfacesBibTeX
@misc{whataifound-axiommath-2026-hypersurfaces,
title = {Browning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literature},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Axiom Math. Verification: Claimed. Autonomy: AI-assisted.},
url = {https://whataifound.org/finding/2026-09-16-browning-sawin-hypersurfaces}
}