Post #1639309

@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.