vim-metamath

Vim-metamath is a vim mode for editing metamath files. Metamath is a language that can express theorems in abstract mathematics, accompanied by proofs that can be rigorously verified by a computer program. Vim-metamath is a vim mode that provides immediate feedback while you're editing metamath files using the widely-used vim text editors. This mode should help you detect and fix defects before you even save your file. It is Free / libre / open source software, released under the MIT license.

Unlike marnix/metamath.vim mode, this vim mode is much more ambitious and strives to differentiate many different things. For example, it specially highlights different kinds of comments inside a comment area, and it colorizes certain operators differently. This creates a lot of visual differentiation that makes it easier to distinguish different kinds of information.

See the Metamath Proof Explorer Home Page to see final results generated from a file edited using vim-metamath. This work was inspired by Whitehead and Russell's monumental Principia Mathematica, and contains over 18,000 completely worked out proofs, starting from the very foundation that mathematics is built on and eventually arriving at familiar mathematical facts and beyond. Each proof is pieced together with razor-sharp precision using a simple substitution rule that practically anyone (with lots of patience) can follow, not just mathematicians. Every step can be drilled down deeper and deeper (as hyperlinks) into the labyrinth until axioms of logic and set theory - the starting point for all of mathematics - will ultimately be found at the bottom. Two plus two equals four actually goes quite deep, because that builds on complex numbers which are first built up from more basic constructs.