>I interrogate it, I ask it to back up and replace its jargon, and I force it to be accountable

I do that too when working on software. Here, I did a little bit of that, but it is much harder when I have almost no domain knowledge (aside from understanding the statement of the conjecture), since at each point the LLM might trick me anyway, and it would probably take me a year to understand the concepts enough to tell when what it's saying doesn't make sense.

>Even just keeping the Lean more up to date would have likely saved tokens

That's the conclusion I came to by the final week! But don't underestimate how much Lean needed to be written in the first place to even "catch up" with the reference papers. I had no option to keep it up to date when I started.