Post by @aspensmonster@tenforward.social

2026-09-11 19:21 UTC

@cwebber@social.coop I'm surprised that the letter says nothing of the fact that OpenAI effectively scooped Navier-Stokes by hiring an entire team of mathematics PhDs to steal^W learn from mathematicians that were busy pouring their mental diaries on the problem into Codex. Has that story changed in the past day or two? Standing on the shoulders of human beings that boxed a problem in sufficiently enough to allow brute-forcing a final proof in a formal proof language like Lean isn't nearly as impressive to me as everyone else seems to think it is 🤷

Replies (2)

@cwebber@social.coop 2026-09-11 19:34

@aspensmonster@tenforward.social I'm surprised also. I think there was probably some consensus building amongst the people co-signing the letter, and I am guessing there was some "well how much do we know"... but this is the part everyone agreed on

Open ##5153942
@ahltorp@mastodon.nu 2026-09-11 20:55

@aspensmonster@tenforward.social @cwebber@social.coop If the LLM did all the work, what were the team of mathematics PhDs doing? There is something that doesn’t fit, as usual in LLM matters. Also, brute-force mathematics seems to me like never getting to the concept of multiplication, and instead just being stuck at the ”counting the small squares in the big square” stage. No new abstractions, no new understanding. What good is a proof if it farts in the forest, sorry, if it doesn’t make us understand more?

Open ##5153946