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 - both for starting this, and for covering the previous week. We should get a bot to automate thisā¦)
As an interesting follow-up to the ai-does-maths-using lean4 stubstack comments on Sunday, an llm accidentally uncovers a bug in the lean4 kernel.
Summary by Meven Lennon-Bertrand:
https://lipn.info/@mevenlennonbertrand/116997917683191056
Eta: āsorry-freeā in this case means a complete proof with no trust-me-bro steps or TODOsā¦ the
sorrytactic in lean āprovesā a theorem to be correct even if it is garbage or incomplete. More programming languages should make developers apologise for half-arsing their work.How bad this is, is unclear just yetā¦ probably not the sky actually falling, but not great. Interesting though.
Lean was already known to be untrustworthy and bad, although people refuse to internalize the situation because theyāre caught up in Buzzardās hype machine. This is extremely funny but I donāt see any signs of people waking up and realizing that Lean sucks.
A little bit of plot thickening spotted by abadidea: https://infosec.exchange/@0xabad1dea/117002106099986943
tl;dr, the timeline looks like this:
There was only a day between the first two events, and the non-proof was not where the bugs were discovered. So maybe it was just a coincidence that the chatbot found the bug at the same time, or maybe itās training data included previous investigations into those bugs which it then built upon and that would be a bad thing for other llm generated proofs.
The collatz conjecture is sufficiently famous that enough third-party checking was done to spot the problem. I wonder how much checking would have been done on proofs of less famous and interesting things.
And a follow-up by talia ringer, who observes that there have always been gaps between the type-theoretic underpinnings of things like the lean prover and their actual implementation, and this hasnāt been so much of an issue til now because theorem provers havenāt had the attention of people in high places, and the type-theoreticians have been able to catch up in due course.
https://mathstodon.xyz/@TaliaRinger/117005740997367321
Anyone want to place any bets on whether or nor the big llm companies are going to fund academic research that isnāt obviously mechanisable right now and wonāt yield any clickbait headlines?
See also a question asked today on Math Overflow, āAre we stuck with Lean?ā. The proposed alternative, Metamath, isnāt type-theoretic and thus skips the entire dialogue between type theory and proof assistants.