Future Directions

Right now many desireable features are missing from the program, such as axiom systems, libraries, and scripting capability. However some infrastructure for the eventual scripting capability is already in place. The following screenshot is of a proof with an embedded subproof.

It will soon be possible to run scripts which will produce embedded subproofs. The namespace system was designed with a library in mind, since the namespaces can be used to categorise theorems and prevent naming conflicts.