2026-10-07 03:40 UTC
Replies (4)
-
@Soyweiser@awful.systems 2026-10-07 07:12
It isnt going to just be math, programming, various sites filled with usefull information that are now being closed because they keep being hammered by bots (or ddos attacks if they manage to actively block the bots) etc. What a waste.
-
@lagrangeinterpolator@awful.systems 2026-10-07 13:18
One of the proofs that OpenAI announced yesterday is for a major open problem in the field I’m working in. I tried to read it but it was a completely incomprehensible 100+ page output. I guess the community has to do all the dirty work of figuring out any sort of understanding. (I had known about the results weeks in advance before their official announcement. There is a bunch of more drama there that I won’t get into.) Putting aside the serious possibility of Lean bugs, a lot of people don’t realize that there is ultimately no point in having a machine just generate Lean blobs endlessly. The reality is that mathematicians have always done math for the sake of enjoyment or understanding, and math contributes to society by improving understanding. Still, I am worried about the convenient social arrangement that allowed many mathematicians to do this for a modest living. Anyway, I’m sure it was a good idea to apply the full might of capital for pure math problems, instead of less important social issues like climate change. We even got a more efficient discrete Fourier transform, improved from O(n log n) to, I shit you not, O(n (log n)^0.9999999999999)).
-
@nfultz@awful.systems 2026-10-07 16:43
If it makes you feel better, the applied / empirical side is just as fucked as pure math. My unhappy thought is we spent 30 years as a discipline trying to decontaminate after The Bell Curve dropped and now, AI Murray will haunt me from beyond the grave.
-
@o7___o7@awful.systems 2026-10-07 18:52
First up: thanks for your hard work here in the sneer mines during these ridiculous times! I saw this being ignored on HN and I thought that you might appreciate it: NAVIER–STOKES LOST IN TRANSLATION – WHY LEAN VERIFICATION OF AI AUTOFORMALISATION DOES NOT GUARANTEE CORRECT NATURAL LANGUAGE PROOFS arxiv.org/pdf/2610.08144 (Apologies for shouting!) The authors (who don’t seem to have a problem with LLMs) point out that automatic translation of natural language mathematics into Lean is very hard, actually. They also highlight some examples of such translation errors in the Navier-Stokes “paper” published by OpenAI. They tread lightly and don’t take a position on the correctness of the proof. I also thought the reference to the Solvability Complexity Index (which is new to me) was interesting, and there’s an appendix with an explainer on how the SCI hierarchy is constructed. According to this scheme, autotranslation of natural language proofs is strictly harder than the Halting Problem. This is all beyond my level, but I’d love to see what our local experts think of it.