Post by @lagrangeinterpolator@awful.systems

2026-10-07 13:18 UTC

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)).

Replies (4)

@istewart@awful.systems 2026-10-07 16:47

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)). rational investors enabling marginal utility… thasss capitalism in action baybeeeee

Open ##4952196
@blakestacey@awful.systems 2026-10-07 16:49

I guess the community has to do all the dirty work of figuring out any sort of understanding. Hooray for the Denial of Service attack from the industry that wants to put a meter on thinking itself.

Open ##4952207
@Amoeba_Girl@awful.systems 2026-10-07 22:21

I’m not at all a mathematician and mostly bad at understanding things, but, is an unwieldy proof that’s barely comprehensible and might be relying on multiple layers of bugs and traps and whatever undefined edges of formal proof systems even a proof at all? Does it actually merit consideration outside of pure spite (understandable)?

Open ##4953908
@fullsquare@awful.systems 2026-10-08 07:22

so what i’m getting from this is the only kind of progress openai and friends are capable of is progressing from slop grenades to slop airstrikes, and so far it only works because they have good marketing, augmented by their own bot farms, and because money is all you need, and so far they haven’t ran out of money

Open ##4956653