Interactive demo walkthrough of basic direct proof.
New example of simple proof by cases. This is part of work in
progress toward additional styles of proof.
Fix deficiencies in the “repetitive number” puzzle.
09/2025
Updated site structure for clarity of purpose and navigation.
Proof builder performance and resource usage both greatly improved.
Many incremental improvements in proof builder user interface.
Full user interface support for exponentiation. While ‘**’ is still
accepted, ‘^’ is the official symbol for it.
Interactive demos of forward and goal-directed proof.
Miscellaneous updates to content.
07/2024
The entire proof builder system is now converted from JavaScript to
Typescript and compiles with minimal errors.
The axiom of induction now properly contains an internal quantifier.
The inference rule / command that sets up an induction proof now
imports relevant assumptions into the scope of the quantifier.
In proofs that have a goal, steps with the goal’s conclusion highlight
undesired assumptions in red to indicate that they need to be proved true.
There is now a formal “subgoal” rule. This allows induction proofs to
stay the same as before except for use of an official subgoal in
proving the inductive case.
Improvements to manual and automatic simplification.
Numerous improvements to presentation of rules in menus and proof displays.
05/2024
New “detach” inference rule. Selecting the conclusion of a step
searches for facts with assumptions it matches. The rule
substitutes into the fact, then removes it as true.
