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 so 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.)
My colleagues in math are now frightened about the (very expensive) mathematical theorem proving ability of these AIs, and many of them really do think that if they can do math, they can do all cognitive tasks. Running a store like this should be so easy! Every single conversation about AI with them has become more frustrating. They are so confused when I still say that the AI companies will die a painful death. When I give my usual points about their expense and their failures in other domains, I am given the usual spiel of “it’ll get better in other areas” and “it’ll get cheaper”.
Unlike them, I have actually been paying attention to this stuff from the beginning. What they think is going on is AI solving math first and shortly getting around to all the other stuff, but what I’ve seen is that AI labs had already tried all the other stuff first and only managed to win the booby prize of theorem proving, which doesn’t pay the bills. And what’s the point of spending thousands or millions to output random blobs of Lean that technically compile if there is no one around to bother making sense of them?
One example I gave is when Anthropic vibe coded an entire C compiler from scratch back in February, which turned out to be a pile of shit. I’ve said that if AI had made similarly rapid progress on software engineering, we would have seen Anthropic continue to put out these demonstrations, and they would have become truly high quality. They would release a compiler more efficient than gcc one week, and a browser better than Chrome the next. (OpenAI’s actual attempt at a browser didn’t go so well.) And if they could do this, they would actually have a shot of making money!
If they could do this, they would have already. The theorem proving stuff actually works (for certain things, in certain ways, at enormous expense), and look at how OpenAI and Anthropic do not hesitate to snipe mathematicians for results rather than being content as tool vendors. But lately I haven’t heard of any software demonstrations. Silence is much louder than noise. More Millennium prize problems bashed with tens of millions in compute costs are not going to change my mind very much.
The counterargument I got was that AI can already one-shot most programming tasks and I shouldn’t be cherry-picking the failures. I am far too tired to argue at this point.
This increasingly seems like one of those “priors” that people should “update on.” One tell is that the leading chip design firm has abandoned sensible power consumption targets, and gone all-in on shoving as much power as possible into as physically large a chip as they can possibly reliably get out of the fab. (Of course, you wouldn’t notice this unless you work in a data center or can afford the more expensive desktop hardware.) I’m trying to think of a pithy catchphrase for social media purposes; best I’ve got so far is that there’s a huge amount of people who have stranded themselves below the upper knee of the S-curve.
There’s a huge difference between having a single counterexample and having a theory that explains where and why counterexamples occur, and what constraints are needed to avoid them. The former are rubies; the latter, wisdom.
I’m disappointed in the maths community but not regretting my decision to avoid taking maths as a major. This is remarkably in line with the mentality cultivated by the typical maths department and must be a frustrating daily experience.
If you ever reopen the topic with your colleagues, an interesting starting point might be their thoughts on theorem 14 from this suite; in my opinion, Lean 4 is clearly untrustable. The lack of awareness of this issue seems to stem from the same blind spot that leads to lack of awareness of non-mathematical cognition: whaddaya mean it doesn’t all reduce to one particular pile of symbols which all fit together perfectly?
Theorem 13 lead to a recent inconsistency
It sounds like many of these math proofs that AI is managing are simply scooped from users’ chat histories anyway!