Want to wade into the sandy, spooky surf of the abyss? Have a sneer percolating in your system but not enough time/energy to make a whole post about it? Go forth and be mid: Welcome to the Stubsack, your first port of call for learning fresh Awful youāll near-instantly regret.
Any awful.systems sub may be subsneered in this subthread, techtakes or no.
If your sneer seems higher quality than you thought, feel free to cutānāpaste it into its own post ā thereās no quota for posting and the bar really isnāt that high.
The post Xitter web has spawned soo many āesotericā right wing freaks, but thereās no appropriate sneer-space for them. Iām talking redscare-ish, reality challenged āculture criticsā who write about everything but understand nothing. Iām talking about reply-guys who make the same 6 tweets about the same 3 subjects. Theyāre inescapable at this point, yet I donāt see them mocked (as much as they should be)
Like, there was one dude a while back who insisted that women couldnāt be surgeons because they didnāt believe in the moon or in stars? I think each and every one of these guys is uniquely fucked up and if I canāt escape them, I would love to sneer at them.
(Credit and/or blame to David Gerard for starting this. The spooks are well underway.)
Unhappy thought: For whatever future weāve got, the history of mathematics will be scarred by fashtech cocaine. The people with all the money have every incentive to make mathematics intractable as a profession. No time or resources to do anything but clean up after their DDOS attacks. No way to check the correctness of AI-generated proofs except by using more AI to formalize them.
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)).
Edit: Here is an article by Quanta which I think accurately describes the situation that mathematicians are going through right now: https://www.quantamagazine.org/is-ai-the-end-of-math-as-we-know-it-20261005/
Hooray for the Denial of Service attack from the industry that wants to put a meter on thinking itself.
rational investors enabling marginal utilityā¦ thasss capitalism in action baybeeeee
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)?
personally I feel like all this shit is a continuation/outgrowth from the crypto āwhitepaperā phenomenon: ~zero substantive engagement with the actual discipline in question, and āwork productā (quotes intentional) equal to some claims with a āproofā thrown out as its defense
(it also continues to be part of a cultural and knowledge DDoS, which others have written better on)
Like, in other words, I donāt think most mathematicians are particularly interested in building huge datacenters to brute-force compute quintillions of decimals of pi under current algorithms? Because the point is understanding, not mere knowledge? I dunno!
If itās actually exploiting a bug in a formal system, no. If itās a natural-language (unformalized) document which no one can understand, no. On the other hand a formal proof not using bugs which canāt be understood, is still considered a proof, though its value is lower than an understandable proof (because as you said in another comment, the real value is in understanding rather than theorems). The prototypical example before LLMs was the proof of the four-color theorem which relied on computer-checked casework.
I suppose what it comes down to is, if OpenAI couldnāt be bothered to try and elucidate their results, or even try to separate nonsensical exploits from genuine proofs, I donāt understand why mathematicians shouldnāt treat all of it as worthless instead of doing unpaid PR work for them.
I think the problem, from a laymanās perspective, is that it wasnāt until the mathematicians started digging through it that it became apparent how bad the situation was. My only frame of reference for whether the proofs are nonsense or not is you kind folks bitching about it, and OpenAI was happy to do the marketing part with or without anyone signing on.
This was exactly the point - flood the zone with shit to show how āsmartā the stuff underlying your IP is
I mean, I donāt know, my confusion comes from also seeing a lot of mathematicians react as if mathematics are over and that it sucks that the future is all about checking AI proofs. And I suppose itās unpleasant when a sort of maybe authoritative entity comes out of nowhere and tells you the answer to your favourite problem is 42 and doesnāt elaborate. But I feel like I might be missing something as to why this is a big deal. (Apart from OpenAIās shitty conduct, I mean.)
I imagine that itās the same thing that programmers have been dealing with. Basically everyone Iāve talked to has acknowledged that code reviews are important parts of the software development process, but nobody has ever said they like them. Now here comes the glorious LLM future where in order to maximize productivity you get to do nothing but code reviews forever, only worse because the answer to āwhat were they thinking when they wrote thisā is always ālmao fuk uā. Even ignoring what kind of consequence that kind of change would have on the actual progress of the field of mathematics, it also just makes being a mathematician into a different kind of day-to-day job, and one that most people who are currently in the field would likely find far less satisfying. And unlike the programmers theyāre not even paid some absurd amount of money for it [citation needed].
Place like /r/singularity and hackernews are eating up the hype and buying into it. Even with mathematicians explaining carefully the errors in the proofs and why they are badly written and useless to actually progress in mathematics the boosters are treating that like sour grapes or irrational fear. If mathematicians tried outright ignoring it, OpenAIās narrative would go even more unchallenged.
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
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:
https://arxiv.org/pdf/2610.08144
The authors 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, but they do bring a large stack of receipts.
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, autoformalisation of natural language proofs is strictly harder than the Halting Problem.
I havenāt had a chance to check on the bona fides of the authors.
This is all beyond my level, but Iād love to see what our local experts think of it in light of the recent gish galop.
Thereās apparently an āAssociation for Human Mathematicsā that has released the following statement:
Stuff like this highlights that the "info"dump was an act of contempt toward professional mathematics. If OAI actually gave a damn about people, they could have coordinated with actual researchers in the relevant fields to clean up the documents while putting a human face on them. Put everything behind NDAs, fund some grants and fellowships, and if it leaks? So what, it would have been actual good press and built hype. Plus, it would have weeded out the the obvious garbage and theyād have brought a lot of young researchers inside the tent.
But nooooooo, they chose violence, because they are assholes. Theyāll never forgive the academics for doing the work and actually being good at math and physics.
I know Iām preaching to the choir, but damn Iām stirred up.
If they actually gave a damn about people they wouldnāt be working at OpenAI
Happy cake day!
Thanks! :)
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.
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.