Interactive math proof system

Question

I'm looking for a tool (GUI preferred but CLI would work) that allows me to input math expressions and then perform manipulations of them but restricts me to only mathematically valid operations. Also, the tool must be able to save a session and later prove that the given set of saved operations is valid.

Note: I am Not looking for a system to generate proofs, only that check that the steps I manually specify are valid.

I have used ACL2 for similar operations and it does well for some cases but it is very hard to use for everything else.

This little project is my motivation. It is a D template type that allows for equation solving. Given this equation:

(A * B) = C + D / F;

Any one of the symbols can be set as unknown and evaluating that expression will result an an assignment to that variable. It works by building expression trees into the type and then using rewrite rules to convert it to something that can be eventuated for the unknown type.

What I need is some way to validate the rewrite rule. They can be validated by testing the assertion that given some relation is true, another one is also.

Answer 1

ACL2 is notorious -- we used to say it was an expert system, and so could only be used by experts, who had to learn from Warren Hunt, J Moore, or Bob Boyer. The thing you need to do in ACL2 is really really understand how the proof system itself works; then you can "hint" it in directions that reduce the search space.

There are several other systems that can help with this kind of thing, though, depending on what you're trying to do.

If you want to work with continuous math or number theory, the ideal is Mathematica. Problem is you can buy a used car for the same amount of money (unless you can qualify for an academic license, a far better deal.)

Something similar, and free, is Open Maxima, which is an extension of Macsyma. That page also points to several others like Axiom, that I've got no experience with.

For mathematical logic operations, there's PVS from SRI. They've got some other cool stuff like model-checking in the same framework.

Answer 2

In addition to what Charlie Martin's links, you may also want to check out Maple. My experience with such software is about 5 years old, but I recall at the time finding Maple to be much more intuitive than Mathematica.

Answer 3

There's ongoing research in this area, it's called "Theorem proving in computer algebra".

People are trying to merge the ease of use and power of computer algebra systems like Mathematica, Maple, ... with the logical rigor of proof systems. The problems are:

• Computer algebra systems are not rigorous. They tend to forget side conditions such as that a divisor must not be 0.

• The proof systems are hard and tedious to use (as you have discovered).

Answer 4

An old and unmaintained system is 'Ontic':

http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html

Answer 5

Several American proof assistants were mentioned already (usually with LISP syntax), so here is a Europe-centric list to complement that:

• Coq

• Isabelle

• HOL4

• HOL-Light

• Mizar

All of them are notorious for TTY interfaces, but Coq and Isabelle provide good support for the Proof General / Emacs interface. Moreover, Coq comes with CoqIDE, which is based on OCaml/GTK an the on-board text widget. Recent Isabelle includes the Isabelle/jEdit Prover IDE, which is based on jEdit and augmented by semantic markup provided by the prover in real-time as the user types.

Answer 6

The lean prover is interactive through a JS gui.