Post #1471251
2026-04-17 13:37 UTC
Replies (5)
-
@carloangiuli@mathstodon.xyz 2026-04-17 13:40
@maxsnew "formalising a textbook is arguably easier...because the answers to everything are in the text" uhhhh what
-
@gallais@mamot.fr 2026-04-17 15:31
@maxsnew It reads like toxic "git gud" gamer chat
-
@koronkebitch@types.pl 2026-04-17 16:42
@maxsnew wow I'm loving that not only do we now have to deal with people saying "have you used the latest model" to "you're not good enough/not using enough agents" fml
-
@MonniauxD@social.sciences.re 2026-04-17 16:44
@maxsnew What was he arguing against?
-
@liamoc@types.pl 2026-04-18 13:51
@maxsnew a student I work with (not my direct advisee) had access to big tech levels of hardware and threw multiple LLMs at a proof problem she was working on. It was so unsuccessful (and this is with big tech levels of hardware) that she painstakingly spelled out the proof in excruciating detail by hand and then fed it to the LLM, and it was able to convert that into an Isabelle proof after a long time getting it totally wrong. Our conclusion was that it would have probably taken less time (and certainly fewer resources) to just do the proof oneself. It's amazing the gap between what these boosters claim LLMs can do and what they actually can do.