Discussion

Completing the formal proof of higher-dimensional sphere packing

robinhouston: I’m not an expert on this subject, but I get the impression this is a pretty significant milestone. This is a major result that won Viazovska the Fields Medal fairly recently, with a reasonably complicated proof, apparently formalized entirely autonomously.

nextos: Jeremy Avigad has discussed this in a short preprint [1]:Gauss’s success was built on almost two years of creative work, scaffolding, and planning by the human participants, and it would have been unfair to them, mostly early-career researchers, to advertise this as solely a success for AI. A bigger concern was that the company would proclaim the project “done.” The formalization, on its own, is close to worthless, since the correctness of Viazovska’s result was never in doubt.It looks like the formalization process of this result is a very interesting case of human-AI cooperation. I am very positive about the same kind of cooperation in software engineering, given that proofs = programs. Lots of boring stuff can be automated, making formal methods cheap enough to become widely used.I said this here two or three years ago and I received some interesting feedback, but in more mainstream venues people thought this was nuts. With a homebrew quirky setup and a fine-tuned LLM for Isabelle and Dafny I have been able to reduce my formalization time by a factor of 5-6.[1] https://www.andrew.cmu.edu/user/avigad/Papers/mathematicians...

ThrowawayTestr: What would sphere packing in one dimension look like?