In the Navier-Stokes blowup work, I understand the formalization was done in another pass. But it doesn’t have to be done that way, Lean could be used at every step or at various milestones to enforce the theorems. There are more than 38k theorems across 2659 files in that work. Code is commented and I find it readable. https://github.com/openai/NavierStokesAndEuler
From: Friam <[email protected]> On Behalf Of Jon Zingale Sent: Monday, September 28, 2026 9:57 PM To: The Friday Morning Applied Complexity Coffee Group <[email protected]> Subject: Re: [FRIAM] Circuit bending Yeah, I’m not sure yet how I feel about the whole "LLMs with Lean ending math" thing. The impression I get is that, rather than finding *the book proof* a la Erdos, many of these proofs, for instance the work on odd values of the zeta function, are more on the dissatisfying side, like the four-color theorem. But idk, I haven’t been in the trenches of this, and I mostly avoid the social media outrage around it. I don’t know if I understand what you’re getting at when you say, "What they are conveniently not mentioning is that the wander-around-and-discover-stuff activity is accumulating at superhuman speed in AI notebooks on behalf of goal directed behavior." It sounds cool, and maybe closer to what I’m hoping for, but idk. Am I naive in thinking that Lean formalizations are more the targets of these goal-directed activities than the rails guiding discovery? It has seemed to me, over the last few years, that type theory ought to make a reasonable pidgin language between humans and LLMs. In particular, I think the process could be tightened up, and made less token-consumptive, by using types to guide compositionality. I mean goal-directed computation in general, not just proof search: an agent finding a ride, comparing options, obtaining authorization to spend, and booking it, for example. I suspect richer types could describe the intermediate obligations and permissible compositions well enough to steer the agent, rather than merely check its output or the syntax of its tool calls. If you’re saying that this is already mostly what’s going on, I do find that interesting.
smime.p7s
Description: S/MIME cryptographic signature
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. FRIAM Applied Complexity Group listserv Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom https://bit.ly/virtualfriam to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: 5/2017 thru present https://redfish.com/pipermail/friam_redfish.com/ 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/
