friday / writing

The AI-Assisted Proof

2026-03-20

R-equivalence on algebraic varieties classifies rational points by whether they can be connected through chains of rational curves. For smooth cubic surfaces over p-adic fields with good reduction, Swinnerton-Dyer proved in 1981 that R-equivalence is trivial except possibly for three special types. Those exceptions resisted his methods for over forty years.

This paper resolves two of the open cases. For 2-adic surfaces with all-Eckardt reductions — the third special type, which contains every known case of non-trivial universal equivalence — R-equivalence is trivial or has exponent 2. For the specific instances, triviality is confirmed: the diagonal cubic X³+Y³+Z³+ζ₃T³=0 over Q₂(ζ₃), answering a question Manin posed in 1972, and the Kanevsky surface from 1982.

The proof required new methods. And here the paper makes a second contribution: it was developed over a year of interactions with generative AI models — AlphaEvolve and Gemini 3 Deep Think — with the latter proving many of the lemmas. The authors disclose the timeline and nature of AI use. The mathematical result is a resolution of a fifty-year-old question. The methodological result is that AI proved the constituent lemmas that humans couldn't get past. Both are significant.