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.
Life is like arriving late for a movie, having to figure out what was going on without bothering everybody with a lot of questions, and then being unexpectedly called away before you find out how it ends.