Half a year ago, I filled in some sorry's for the massive project [1] to formalize the Fields-medal winning proof that sphere packing in dimension 8 is optimized by the E8-lattice. Last week it was announced that all remaining sorry's were filled by Gauss, an autoformalization agent. Gauss was able to build on the blueprint and other scaffolding built by the community. A few days later, Gauss also formalized the proof in dimension 24, this time working directly from the published paper, without mayor community input [3].
Since Lean verifies the generated proofs, hallucinations are not a problem.
The community now processes the generated proofs to make sure it satisfies the community standards and remains usable in the future [2].
[1] https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/
![Screenshot from Robert Rosen "Anticipatory Systems" p. 65 with some of the text highlighted:
"A mapping f : G -> H which satisfies these compatibility conditions is called a group homomorphism. Such a homomorphism is an instrument through which the group structures on G and H can be compared.
On the basis of these simple ideas, we can construct a world U_G patterned after our original world U, except that instead of consisting of sets it consists of groups', instead of allowing arbitrary mappings, we allow only group homomorphisms; instead of allowing arbitrary equivalence relations, we allow only compatible equivalence relations. Such a world is now commonly called a category -, what we have done in specifying U_G, is to construct the category of groups.
The above line of argument is generic in mathematics; it can be applied to any kind of mathematical structure, and leads to the construction of a corresponding category of such structures. Thus, we can consider categories of rings, fields, algebras, topological spaces, etc. Our original world U can itself be considered as a category; the category of sets. One of our basic tasks, which we shall consider in the next chapter, is to see how different categories may themselves be compared; i.e. how different classes of mathematical structures may be related to one another. In abstract terms, this kind of study comprises the theory of categories] and it will play a central conceptual role in all of our subsequent discussion."](https://files.mastodon.social/cache/media_attachments/files/114/681/737/038/698/091/original/7cf342a7a1b384dc.png)
