MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics

Abstract

The Emacs authoring environment for Mizar (MizarMode) is today the authoring tool of choice for many (probably the majority of) Mizar authors. This article describes the MizarMode and focuses on the proof assistance functions and tools available in it.

Keywords

• MizarMode
• integrated
• proof
• assistance
• Mizar
• formalizing
• mathematics