2.9.7 Proving — an Art or a Science?

Proving can be quite frustrating for both beginners and advanced users. Beginners sometimes get the impression that proving is just “clicking around” that sometimes works and sometimes does not. When it does work, it’s not really clear why. The proof tree is also difficult to read even for experienced users. We provided some additional guidance on provers in the reference chapter (3.4.5) that may be of help, but keep in mind that proving is a skill that can only be learned by practice. Here we are trying to help you learn how you can use Rodin to solve proofs, but actually teaching you how to prove something is not really in the scope of this document.