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.
Green's Law of Debate: Anything is possible if you don't know what you're talking about.