Get HLM at Fast, secure and Free Open Source software downloads

The HLM Proof Assistant

Screenshot 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

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

Mathematical Features


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