keeganryan

This builds on the Kickmix quantum language from Google. Essentially, Kickmix is an assembly language for classically simulatable quantum circuits, and finding more efficient circuits is basically a game of code golf with the assembly instructions. That means LLMs benefit from the closed loop of verification, and can rapidly test and discard ideas. It's not too surprising that previous academics didn't try to optimize to this level, and a good task to automate. See ecdsa.fail for another example of circuit optimization using the Kickmix language.

Me too. This is the sort of thing that would traditionally be hidden as n lg n ^ (1 - eps) for some eps > 0, but it's much more amusing this way.

No way this is the correct upper bound, and I imagine it'll get refined fairly quickly. IIRC, the GapCVP results were released with a 1/n^400 complexity term, but people quickly got it down to 1/n^8 by more careful accounting.

Yes, absolutely. There's been a lot of work along these lines in other interactive theorem provers like Isabelle/HOL and Rocq. The general term to search is "Hoare logic," and I'm also a fan of the Concrete Semantics textbook. Lean is a very flexible language, but the main downside with Lean is that libraries for reasoning about program logic are comparatively less developed than Mathlib is for math.