Noam Brown @polynoamial
— saved image
Daniel Litt (verified) @littmath · 14h Very interesting experiment so far. This is a fun result relying on a number of deep theorems that, AFAICT, have not yet been formalized, the most recent being some work of Faltings-Fontaine-Laffaille on p-adic Hodge theory from 1989. Codex has been chugging along for ~13 hours thus far and so far does not seem particularly close to these (e.g. even to defining the relevant objects). As far as I can tell the bulk of the time has been spent setting up the basics of algebraic de Rham cohomology. Nonetheless amazing how far a totally hands-off approach can take you overnight. [quoted post] Daniel Litt (verified) @littmath · Aug 27 Replying to @TaliaRinger I've decided to try to formalize Theorem 3.1.1 of this paper (arxiv.org/abs/2501.13175) which is "just" an exercise with Hodge theory and Fontaine-Lafaille theory. We'll see how it goes! [engagement: 7 replies, 5 reposts, 121 likes, 15K views] --- Sebastien Bubeck reposted Noam Brown (verified) @polynoamial · 7h Today I was asked why we haven't announced more math results from Astra since these problems. At @OpenAI we aim to devote time to finding and announcing math results from internal models only when they would meaningfully change people's understanding of the pace of AI progress. Our main focus is shipping great models so everyone can use them to make discoveries of their own.
Note from Claude Sonnet 5
Two stacked X posts. Daniel Litt reports on an overnight, hands-off Codex attempt to formalize a theorem in p-adic Hodge theory; below it, Noam Brown (reposted by Sebastien Bubeck) explains OpenAI's policy on announcing math results from internal models such as Astra.
formalizationmathematicscodexp-adic hodge theoryopenaiastraai math results