Jared Duker Lichtman

We are pleased to share that using Gauss, we have completed a ~200K LOC formalization of Maryna Viazovska’s 2022 Fields Medal theorems on optimal sphere packing in dimensions 8 and 24. This is the only Fields Medal-winning result from this century to be completely formalized, and is the largest single-purpose Lean formalization in history. We are honored to have assisted @SidharthHarihar1 and the rest of the sphere packing team in this achievement. math.inc/sphere-packing

Today, at the @DARPA expMath kickoff, we launched 𝗢𝗽𝗲𝗻𝗚𝗮𝘂𝘀𝘀, an open source and state of the art autoformalization agent harness for developers and practitioners to accelerate progress at the frontier. It is stronger, faster, and more cost-efficient than off-the-shelf alternatives. On FormalQualBench, running with a 4-hour timeout, it beats @HarmonicMath's Aristotle agent with no time limit. Users of OpenGauss can interact with it as much or as little as they want, can easily manage many subagents working in parallel, and can extend / modify / introspect OpenGauss because it is permissively open-source. OpenGauss was developed in close collaboration with maintainers of leading open-source AI tooling for Lean. Read the report and try it out:

Today, at the @DARPA expMath kickoff, we launched 𝗢𝗽𝗲𝗻𝗚𝗮𝘂𝘀𝘀, an open source and state of the art autoformalization agent harness for developers and practitioners to accelerate progress at the frontier. It is stronger, faster, and more cost-efficient than off-the-shelf alternatives. On FormalQualBench, running with a 4-hour timeout, it beats @HarmonicMath's Aristotle agent with no time limit. Users of OpenGauss can interact with it as much or as little as they want, can easily manage many subagents working in parallel, and can extend / modify / introspect OpenGauss because it is permissively open-source. OpenGauss was developed in close collaboration with maintainers of leading open-source AI tooling for Lean. Read the report and try it out:

"There's something about this culture of young people coming up where they're not afraid of hard work. They're not afraid to pop a Zyn and work at the factory all day." Why @KTmBoyle is bullish on Zoomers: "The best quote that summarizes why I'm so bullish on the Zoomers is Alysa Liu after winning her gold. She said, 'I love to struggle. It makes me feel alive.'" "It's the opposite of the morose theater kid vibes that we got from the millennial generation, where everything was very different in how they operated." "Like Jack Hughes—they get their teeth knocked out, they come back and say, 'It's not even a question. Of course I got my teeth knocked out. It's hockey.'" "And that means we're seeing totally different companies than we saw out of the Facebook diaspora—which was very much the Harvard dorm room—I like to work on my computer, I like to build apps. It's a totally different style of founder." "The next generation is so patriotic and bullish on the American project. I think this generation cares a lot about the country. And it shocked us. @davidu and I talk about this all the time—for some of these young people, they were not born on September 11th. They have no recollection of the things that the millennials remember, or anyone older than us remembers, but they care about the country." "They look up to people like @elonmusk, to people like Alex Karp. They look up to people who've been doing the hard thing for 20, 30 years and they want to do it too." "It's a different generation of founder that we've had the privilege of seeing very, very early on. I think the rest of the country is going to define tech and Silicon Valley by these people for the next 10–20 years." From @nypost

@unsorsodicorda Yes, I’m curious to see what kind of progress will be made. Buzzard had an ongoing project (pre-autoformalization) which aimed to formalize large parts of the argument “by hand” in 5 years, which gives a sense of the magnitude.