---
name: "metamath"
section: "1"
platform: "linux"
package: "metamath"
version: "0.195-1"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/metamath"
---

# metamath(1)

Formal proof verifier and proof assistant

## NAME

metamath - Formal proof verifier and proof assistant

## SYNOPSIS

**metamath \[** *commands* **\|** *file* **\]**

## DESCRIPTION

**metamath** is a formal proof verifier and proof assistant for the Metamath language. It can be initialized via a series of *commands* or with a data base *file*, which can then be explored interactively.

For details about the Metamath language and the command-line interface, type **help** into the command prompt, or read the Metamath book \[1\], which should have been installed along with the package.

## LANGUAGE

A Metamath database consists of a sequence of three kinds of tokens separated by white space (which is any sequence of one or more white space characters). The set of keyword tokens is **${**, **$}**, **$c**, **$v**, **$f**, **$e**, **$d**, **$a**, **$p**,  **$.**, **$=**, **$(**, **$)**, **$\[**, and **$\]**. The latter four are called auxiliary or preprocessing keywords. A *label* token consists of any combination of letters, digits, and the characters hyphen, underscore, and period. The label of an assertion is used to refer to it in a proof. A math *symbol* token may consist of any combination of the 93 printable [**ascii**(7)](/ascii/7.md) characters other than **$**. All tokens are case-sensitive.

- **$(** *comment* **$)**

  Comments are ignored.

- **$\[** *file* **$\]**

  Include the contents of a *file*.

- **${** *statements* **$}**

  Scoped block of statements. A math symbol becomes active when declared and stays active until the end of the block in which it is declared.

- **$v** *symbols* **$.**

  Declare *symbols* as variables. A variable may not be declared a second time while it is active, but it may be declared again (as a variable, but not as a constant) after it becomes inactive.

- **$c** *symbols* **$.**

  Declare *symbols* as constants. A constant must be declared in the outermost block and may not be declared a second time.

- *label* **$f** *constant variable* **$.**

  Variable-type hypothesis to specify the nature or type of a variable (such as \`let x be an integer.'). A variable must have its type specified in a **$f** statement before it may be used in a **$e**, **$a**, or **$p** statement. There may not be two active **$f** statements containing the same variable.

- *label* **$e** *constant symbols* **$.**

  Logical hypothesis, expressing a logical truth (such as \`assume x is prime') that must be established in order for an assertion requiring it to also be true.

- **$d** *variables* **$.**

  Disjoint variable restriction. For distinct active *variables*, it forbids the substitution of one variable with another.

- *label* **$a** *constant symbols* **$.**

  Axiomatic assertion.

- *label* **$p** *constant symbols* **$=** *proof* **$.**

  Provable assertion. The *proof* is a sequence of statement *label*s. This label sequence serves as a set of instructions that the Metamath program uses to construct a series of math symbol sequences. The construction must ultimately result in the math symbol sequence contained between the **$p** and **$=** keywords of the **$p** statement. For details, see section 4.3 in \[1\]. Proofs are most easily written using the interactive prompt in **metamath**.

## FILES

*/usr/share/metamath*

Data base files for several formal theories.

## SEE ALSO

**\[1\]** Norman Megill: Metamath, A Computer Language for Pure Mathematics ⟨http://us.metamath.org/downloads/metamath.pdf⟩.