Because conjectures are often flawed, LP is not designed to find difficult proofs automatically. For example, LP does not use heuristics to formulate additional conjectures that might be useful in a proof. Instead, LP makes it easy for users to employ standard techniques such as simplification and proofs by cases, induction, and contradiction, either to construct proofs or to understand why they have failed.
LP also provides support for rechecking proofs following changes in axioms, conjectures, or proof strategies. This support assists users in regression testing during proof construction: when users discover they must change a formalization in order to establish some conjecture, regression testing ensures that the change does not invalidate previously constructed proofs. This support also promotes proof re-use: users can edit old proofs to prove new conjectures, and LP will check that the progress of the proof stays ``in sync'' with the users' intentions.