> Compare to software verification: when you prove a sorting algorithm correct, the hard work is the loop invariants and the model, not the final QED. Tedious proof steps usually indicate you're fighting your abstractions.
This is a false statement when working with an interactive theorem prover like Lean. Even trivial things require mountains of effort, and even blatantly obvious facts will at least require a case analysis or something. It's a massive usability barrier (and one that AI can hopefully help with).
This is a false statement when working with an interactive theorem prover like Lean. Even trivial things require mountains of effort, and even blatantly obvious facts will at least require a case analysis or something. It's a massive usability barrier (and one that AI can hopefully help with).