Actually automated theorem provers like Lean are the PERFECT use for LLMs because you can instantly determine if the proof it generated is correct.
A "two-page document" (perhaps 200-300 lines of code) would typically check in a matter of seconds to, at most, a few minutes. If it took hours, it would mean the file contains a pathological case that a developer would be expected to identify and fix. It is absolutely not a normal or "not unusual" occurrence.
1. Load a complex data structure, e.g. from JSON. (I do not consider typing out the JSON to be part of the human's job.)
2. Process the data, using the magic of functional programming. (Performance? What's that? Performance is not a priority.)
3. Add some helpful lemmas.
4. Prove the data processing stage was correct… but proving this in general is haaaard, so just make automation that's capable of proving it for most cases… eventually.
5. Great! It takes 3 minutes to run on my tiny examples. Now run it on the real data.
And that's where hours come from!
> Lean's metaprogramming capabilities enable users to extend the language with domain-specific notations and new proof automation techniques.