Saw this on the FOM mailing list, unfortunately the archive is down, so the posting verbatim below

I just proved that marked ruler and compass solve the general quintic equation.

Conway and I often talked about this problem. He’d have been so pleased to see I finally found the construction he was sure was there.

Needs one Tschirnhaus transformation to remove x^2 and x^4 terms, one double neusis using compass as a divider with same unit radius as the marks on the rules, and a bunch of square roots.

Claude Opus and ChatGPT Sol helped a lot with the algebra, if I’d been a tenured professor I maybe could have done it in a year of work without them, but I never had that year. The difficulty was using algebraic geometry intensively to figure out why all the searches were failing, so that I could finally search along the right kinds of constructions. Being able to get Galois groups and factorizations of polynomials and more advanced arithmetical information quickly for thousands of equations would have been enough for an algebraic geometer, but I needed to learn the algebraic geometry too and the LLMs were ideal for that, as well as speeding up the algorithm development by 10x or so.