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.)
You know how AI proofs are supposed to be credible because of formalization with Lean? The AI generates a natural language proof and then supposedly generates a Lean program corresponding to the proof to verify that it’s true. There is now some troubling news about that: there are frequent examples where the statement given in natural language is different from the meaning of the Lean formalization.
The paper even points out several obvious mismatches in OpenAI’s famous Navier-Stokes solution between the English proof and the Lean formalization. There is even a spot where a 4 in the English proof turns into a 5 in the Lean proof (which causes further problems down the line). This is mostly a cosmetic error, and it doesn’t mean that the Navier-Stokes solution is wrong, but there could very well be deeper problems, especially with the English proof. At minimum, this solution absolutely requires careful review by experts. OpenAI’s behavior towards said experts has been appalling.
My viewpoint has been that the only successes that AI has had are in domains where failure is not costly (at least for someone with deep pockets), and especially when there is a formal system such as Lean that can reliably catch errors. So AI can be endlessly trained to write compiling Lean programs corresponding to formal proofs, but as soon as it runs into tasks that are not 100% bolted down, like writing the proof in English, the hallucination problem rears its ugly head. This reinforces my belief that AI is a chess engine but for Lean.
If I was treating this as a technical problem, I would say, why not just have an AI that generates the Lean proof, and at most have an optional assisting tool that translates it into English without perfect reliability? But this is not a technical problem. By outputting English proofs in the format of a research paper, 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).