What fullsquare said, they’ve got years of sci-fi filtered through lesswrong short stories and sequence posts saying it could happen, so they repeated that despite all the ways it is completely impossible given the limitations and hardware requirements of LLMs.
One of the classic sequence posts plays with the concept: https://www.lesswrong.com/posts/5wMcKNAwB6X4mp9og/that-alien-message
But in a uno reverse twist, its the humans that are a metaphor for AI, with them manipulating out thinking the aliens from within the simulation.
Someone on Scott Aaronson’s blog suggested math will become an empirical field now, where they run “experiments” by asking AI for lean proofs.
Scott, is this a turning point where mathematics gets off its well trodden path of logic and becomes more like an empirical science? Heck, people were arguing if math is invented or discovered, this settles it. Math is discovered – by AI! From now on forth, Mathematicians will become scientists, wielding AI as a telescope, pointed towards new and disturbing alien worlds in the Platonic realm.
So yeah, it seems like this idiotic view is pretty popular among boosters.
The theory on the thread that
My guess is that this represents a shift in focus at OpenAI away from math: they had their big meaningless trophy prize with the Navier-Stokes solution, they appear to have distanced the competition (Anthropic) and the public bought the notion that “math is solved”
seems like a plausible explanation? I’ll guess we’ll if OpenAI moves on now that they’ve “solved” math or if they follow up with a few more drops of “proofs”.
True, but its a different form of disrespect, where they outwardly steal the style and aesthetics of the discipline to try to claim its legitimacy. Like the endless “whitepapers” pumped out by cryptobros.
I do not see the point of math for AI alone, since I do not think AI is or will ever be conscious.
Rationalists (and in general those with fear/hope or a technological singularity) have the idea that once the AI is smart enough, it will be able to recursively self-improve in an exponential process. Vibe-coding hasn’t made this come true, so they are trying to make it happen by shoving enough of the right sort of knowledge into the AI. Obviously being smart and being mathey go together, so if the AI just gets good enough at math, surely bootstrapping to godhood is just around the corner!
To them, the AI is not here for us, but we are here to serve the AI.
The techbros are giving mathematicians the humanities treatment. (I.e. they don’t respect the entire profession despite its immense importance to actually understanding reality.) Before, mathematics had sort of gotten half a pass for being rigorous and adjacent to stuff techbros do respect, like computer science. But, given just half a whiff of the idea that they may no longer need human mathematicians, they are ready to accept utter slop…
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.
You know how AI proofs are supposed to be credible because of formalization with Lean?
There is another problem… apparently Lean4 hasn’t actually been fully formally verified. And in fact could have more bugs lurking in it, maybe even some foundational problems… Lesswrong post explaining the problems.
OpenAI can more easily market that their AI is intended to fully replace mathematicians, and that this is only the herald of their general superintelligence (and not that math is the only thing working out for them).
Yeah, this has been driving me crazy… reading places like hackernews or r/singularity, I keep seeing people assuming mathematicians and just bitter or engaging in sour grapes and that is why they are complaining about the “proofs” OpenAI dumped out. Like it is just some small niggling detail that the proofs can’t be read by humans and that Lean may have bugs and that some of OpenAI’s proofs have already been shown to have critical mistakes.
Edit: I had the thought to collect some links in one place Here are some more discussions on lean and autoformalization for anyone looking for good sources:
Edit 2: Made a top level post: https://awful.systems/post/9997783
Or cite it, but in the most passive aggressive way you can get away with.
…You should check the literature really carefully to make sure that whatever proof the AI “generated” doesn’t actually already exist somewhere and it regurgitated it without proper accreditation.
Yeah lesswrong is weird about China. Its an ongoing thing. It alternates between fear (that China won’t appreciate the risk of making AI Satan or will beat the US to making AI God) and occasional hope (that they might manage to “safety-pill” China and China will find the magic formula to AI alignment). I pulled together some posts previously here: https://awful.systems/post/4103825
If it had been only a year they’ve been saying that, I might almost buy the logic. But it has been 4 years since Chat-GPT came out and they’ve been making the same promises the entire time.
Something of a tangent… thinking back to 2022-2023 my expectations for what the LLM companies would actually achieve by now were actually too high? Like I would have thought they would have figured out a better architecture for gluing functionality and symbolic logic to LLMs than just calling tools with the output text stream and feeding the tool outputs into the context window.
I also thought of Open Philanthropy, but couldn’t remember the Eliezer post that best illustrated his resentment towards them. (In addition to the top-level post you’ve linked, I’ve seen various bitter lesswrong comments along the same lines).
“a giant rich organization”: they claim to have directed over 7 billion in grants since 2014, so this actually seems like a fair comment?
“stole some of my ideas”: they’ve shown interest in AI stuff, including Eliezer’s ideas, they just have longer (but still pretty fantastical, like AGI by 2050) timelines for stuff like AGI and that influences their funding priorities in a way Eliezer disagrees with
“ignored everything I said about what not to do”: eh, Eliezer has said a lot of things, they probably didn’t follow his advice exactly
“and are going around telling people I made them do it”: I’ve seen a few people here and there in various rationalist-adjacent circles blame Eliezer for helping OpenAI network and get started and thereby kindle the very doom he warned about, so. It seems plausible some of them were connected to coefficient giving?
Its not stealing your ideas if they cite you Yud, they just draw different conclusions
That sounds like the normal academic process, which Eliezer neither understands nor appreciates.
Yud has said he got bored with LessWrong
Yeah, him gradually losing interest in LessWrong in the mid 2010s created room for SSC to grow in popularity. Also, that would have been around the time it became apparent Eliezer had been very wrong about neural networks, so we missed the chance to see Eliezer actually have to overcome biases and admit he was wrong in a non-self-aggrandizing way. (Eliezer has admitted he was wrong before, but only in ways that made his next idea even more important, see his progression from nanotech to coding a seed AI in Lisp to solving AI safety).
They actually both converge to a retelling of SCP-8008.
Not only that, they view commonsense moral and ethical reasoning as a PR constraint, i.e. look at the discourse around the hiring of Caroline Ellison to an EA org that handles significant sums of money. Lot of commenters were merely framing it as a PR problem and not a basic commonsense ethics problem.
Considering how much compensation he gets a MIRI, he could afford to hire an artist out of his own pocket and he would end up with something better and not be funding the technology that he claims is going to kill us all…
I think past AI winters is a somewhat useful analogy, but yeah, I agree, drawing too strong a comparison is misleading.
Likewise for people comparing the AI boom to the dotcom boom and bust. Ed Zitron has ripped into this comparison repeatedly. Basically, the fiberoptics laid by the dotcom boom where useful for decades, whereas heavily used GPUs fail in ~6 years.
The thing about the “yet you participate in society, curious!” meme is that you don’t really get the option to not participate in society. you do however get the option to not participate in AI, and there are plenty of people happily taking that option
Yeah, rationalist utterly fail at understanding collective action, or really anything besides lib-brained centrist methods of action. Well, maybe even lib-brained centrist is giving them too much credit, because even milquetoast liberals will occasionally avoid using products for ethical reasons. See Only Law Can Prevent Extinction, where Eliezer basically explains how all other action besides an international total ban on AI and GPUs is pointless. (I think he is trying to avoid people bombing data centers, but Elizer’s “logic” is also implicitly against stuff like going to town halls to complain about data centers.)
Yeah, the review nitpicks the quality of the AI generated slop, but overall is in favor of doing a better job slopping, not avoiding slop altogether.
Yep, so many of their favorite tropes and assumptions fail when an actual expert breaks them down. Like their belief in the possibility of Drexler-style nanotech has been taken down quite firmly several times (here is a good takedown that got posted to the EA forums), Drexler’s ideas pretty firmly ignore how things actually work at the molecular level…