Comment by vatsachak

Yeah computer proof writing involves choosing good abstractions at every turn. LLMs aren't great at that yet