Christ, you are so correct.

> I’m about 50% of the way through the formalization plan > I think formalizing using AI was way slower than if I’d done it by hand.

combined with their aversion to learning something hard alone:

> I found learning Lean annoying and difficult. So I started looking for shortcuts.

The author failed utterly according to their own definition of success. Moreover, how will they know they have completed the task if they don't want to fully understand what they've 'written'?

The paper presents a false trichotomy:

(1) go to grad school and learn to do it yourself (2) hope one of the few theorem proving experts got interested in your problem (3) give up. and the magical fourth: (4) Look Just Try Claude Code (at just $100 per month!)

"got interested" is so utterly passive, I've got a fifth option. (5) Meet other people who share your interests on discord and forums and chat about the problems you are trying to solve. Make them interested! Nerd snipe them! Make friends, meet colleagues and learn new things while having a genuine human experience, for free!