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]
- 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]
- Tight integration of prover and GUI, making it impossible to even enter
anything invalid.
- 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 arbitrary constraints in definitions ("partiality").
[Screenshot]
- 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."
- 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.
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.