Want to wade into the snowy 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 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.)
This was a very nice problem set. Some were minor alterations to thms in literature but ranged up to problems that were quite involved. It appears that OAI got about 5 (possibly 6) of them but even then, this was accomplished with expert feedback to the model, which is quite different from the models just 1 shotting them on their own.
But I think this is what makes it so well done! A 0/10 or a 10/10 ofc gives very little info, a middling score that they admit they put a shit ton of effort into and tried to coax the right answers out of the models via hints says a lot about how much these systems can currently help prove lemmata.
Side note: I asked a FB friend of mine at one of the math + ai startups if they attempted the problems and he said "they had more pressing issues this week they couldnt be pulled away from" (no comment, :P I want to stay friends with them)
The lack of similar attempts being released by big companies like Google or Anth or X also should be a big red flag that their attempts were not up to snuff of even attempting.
I found the comment about models creating very old-fashioned "18th century style" proofs very interesting. Not surprising in retrospect since older proofs are going to be reproduced more across the training data compared to newer ones, but it's still interesting to note and indicative of the reproduction that these things are doing.
Also Martin Hairer is incredibly based. He gave this nice talk 2 months ago if any peeps want to see what he thinks comes next for math.
https://www.youtube.com/watch?v=fbVqc1tPLos