The HLM Proof Assistant

HLM is a proof assistant intended for abstract mathematics, which is currently under development. It is designed entirely with GUI technology in mind, so that input and output resemble mathematical practice as closely as possible. Although the software is not yet ready to formalize serious proofs, a downloadable prototype highlights its main features and style of interaction.

Technical Features

• Fully graphical editor; no text input required.
• Inline, menu-based editing of sub-expressions according to abstract syntax. [Screenshot]
• Flexible user-definable notation for every definition in the library. [Screenshot]
  (Note: The notation cannot be edited graphically yet.)
• Tree view showing all definitions and theorems of the library graphically, with fast preview of the item under the mouse cursor. [Screenshot]
• Keyword search acting as filter in tree. [Screenshot]
• One-click navigation to the definition of any symbol, with preview. [Screenshot]
• Context-aware list of most-recently used objects. [Screenshot]
• Built-in support for multiple equivalent definitions. [Screenshot]
• Convenient rendering of common mathematical constructs such as implicit definitions, theorems that state equivalences, etc. [Screenshot]
• Combined procedural/declarative proof style: Steps are selected from menus or constructed using dialogs, but displayed in a human-readable way. [Screenshot]
  (Note: The dialogs do not exist yet.)
• Tight integration of prover and GUI, making it impossible to even enter anything invalid.
  (Note: Many rules are not fully implemented yet.)
• Graceful handling of unfinished definitions or proofs: Interrupt a proof to state a missing lemma, then finish the proof, finally prove the lemma.
• Undo possible for all changes.
• XML-based file format for data exchange.
• Optional import into local database, for instant loading of arbitrarily large libraries.
• Independence of the organizational structure of the library from the references between definitions and theorems (to support classification based on topics instead of dependencies).
• Easy reorganization of the library via drag&drop. All move and rename operations automatically update references.
• LaTeX export. [Current library as PDF]

HLM is an open-source (LGPLv2.1) Java application running on Windows, MacOS, and Linux.

Mathematical Features

• Set-theoretical foundation designed to closely resemble mathematical practice.
• "Invisible" type system that eliminates meaningless choices from menus and dialogs. [Screenshot] [Paper of presentation at TYPES'10]
• Based on classical logic. (Support for constructive logic can be added if sufficient demand arises, but requires nontrivial modifications to the software.)
• Support for arbitrary constraints in definitions ("partiality"). [Screenshot]
  (Note: The corresponding "inline" proofs are not available yet.)
• Definitions with bound variables, for faithful formalization of generalized sums and products, limits, derivatives, integrals, etc. [Screenshot]
• Formalization of "standard embeddings" from existing into newly constructed sets (made possible by the type system). [Screenshot]
• Introduction of a mathematical structure (i.e. a definition of "group," "ring," "vector space," etc.) also implicitly defines a set of all isomorphism classes of its instances. No distinction between "sets" and "proper classes" is necessary.
• These sets can be used to construct categories in the sense of category theory. There is even a "category of all categories except itself."
  (Note: Category theory cannot be formalized in the software yet because a rather central mechanism is unfinished.)
• The consistency of the system (as a corollary of soundness with respect to a truth predicate) can be proved in Zermelo-Fraenkel set theory, and in a slightly extended version of the system itself.
  (Note: Since the rules of the formal system are not fully implemented yet, the software is actually inconsistent at this time.)

Feedback

Comments, questions, and requests are always welcome; so is constructive criticism, and (of course) any kind of help. Please contact Sebastian Reichelt at sreichelt@users.sourceforge.net.