American AI startup developing a model called Gauss that can convert human-written mathematical proofs into lines of Lean code. Gauss successfully formalised proofs by Maryna Viazovska for higher-dimensional versions of the sphere-packing problem—for 8-dimensional and 24-dimensional spheres, respectively—within weeks. Even though both proofs had already been verified without AI, Gauss's work contributed to mathematicians' understanding of the tools in Viazovska's proofs.
The problem with most conspiracy theories is that they seem to believe that for a group of people to behave in a way detrimental to the common good requires intent.