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.