Completing the formal proof of higher-dimensional sphere packing(math.inc)
math.inc
Completing the formal proof of higher-dimensional sphere packing
https://www.math.inc/sphere-packing
8 comments
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.
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 quirky homebrewn setup, including a fine-tuned LLM for Isabelle/Dafny, I have been able to reduce my formalization time by a factor of 5-6.
Some minimal formalisms are needed anyway even in case you are not interested in high quality assurance to make sure agents synthesize mostly correct code. IMHO, purely neural agents are much less useful than advertised without some symbolic guardrails.
[1] https://www.andrew.cmu.edu/user/avigad/Papers/mathematicians...
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 quirky homebrewn setup, including a fine-tuned LLM for Isabelle/Dafny, I have been able to reduce my formalization time by a factor of 5-6.
Some minimal formalisms are needed anyway even in case you are not interested in high quality assurance to make sure agents synthesize mostly correct code. IMHO, purely neural agents are much less useful than advertised without some symbolic guardrails.
[1] https://www.andrew.cmu.edu/user/avigad/Papers/mathematicians...
Thanks for the pointer. I already had Avigad’s paper open on my computer, but I haven’t read it yet.
I take the point about the output – as opposed to the process – being “close to worthless”; though I suspect it’s only a matter of time before some result whose correctness ‘was never in doubt’ is found to be incorrect as a consequence of an attempt to formalize it.
I take the point about the output – as opposed to the process – being “close to worthless”; though I suspect it’s only a matter of time before some result whose correctness ‘was never in doubt’ is found to be incorrect as a consequence of an attempt to formalize it.
I agree. The formalization is very impressive even if we consider it was done on a result that is already accepted as true and got a lot of help from humans to scaffold and build the structure.
What would sphere packing in one dimension look like?
Putting as many unit length line segments on a line as you can.