Won’t proofs formal enough for a computer be extremely long?
Sometimes. There are several things that make this less annoying than it sounds.
- Lurch will have a growing number of “shortcut rules” over time. For example, imagine a rule called “algebra,” which would just check to see if an equation you typed was true, according to a built-in computer algebra system. Lurch already has such a rule, alleviating many steps of tedious proving about basic algebra (and arithmetic, trigonometry, calculus, etc.). Such a rule can be enabled and disabled for different documents. Lurch will gain more rules like this one over time (e.g., one for skipping propositional logic proofs).
- Users are always free to skip steps in a proof. The missing steps cannot be validated by Lurch, but if the user is confident that they are correct, they can continue the proof after the skipped step, and ignore Lurch’s red mark at the gap.
- Instructors who do a good job of choosing axioms, rules, and theorems to support the proofs the students need to do can minimize this problem. Consider this algorithm, as an instructor: Write out the proofs you expect your students to do, and look at all the reasons you cited. Make each one into a theorem or axiom, and provide those to your students.