MathCheck Brief Instructions

This document is as of 2021-11-16. It lacks all more recent features of MathCheck.

In ready-made problems, the use of commands may have been restricted to those relevant for the problem.

Arithmetic and Parentheses

`54 frac(3)(21)`54 3/21
`x^(-y z)`x^(-y z)
`\ text(div)\ `div
`sqrt x+1`sqrt x+1
`d/(d x) sin 5x`DD x sin 5x

The input symbols ( and ) denote ordinary parentheses and #( and #) denote hard parentheses. MathCheck removes unnecessary ordinary parentheses, but always prints hard parentheses even if they are unnecessary.

Comparisons and Logic

`\ sf"&&"\ `&&
`\ sf"||"\ `||
`AA x:`AA x:
`AA i; 1 <= i <= n:`AA i; 1 <= i <= n:
`EE x:`EE x:
`EE i; 1 <= i <= n:`EE i; 1 <= i <= n:

Reasoning Chains

A reasoning chain may contain ⇐, ⇔, ⇒ and ≡, and the following:

assume x != 1 /\ y >= x;Set a condition that is assumed to hold throughout the (sub)proof. One may use enda instead of ;.
originalRefers to the first formula in a reasoning chain. If original is the first formula of a subproof, then it refers to the first formula of the parent proof.
subendEnds a subproof.
subproofStarts a subproof.

What formulas in a reasoning chain may contain depends on the problem mode. Typically most logical and comparison operators are allowed, but only a small set of arithmetic operators.

Greek Letters


Lexical Rules

Spaces and newlines may be freely used between tokens. If a non-numeric token ends and the next one starts with a letter or digit, there must be at least one space or newline in between.

These symbols can also be given as Unicode characters: ¬ ² ³ Γ Δ Θ Λ Ξ Π Σ Φ Ψ Ω α β γ δ ε ζ η θ ι κ λ μ ν ξ π ρ σ τ υ φ χ ψ ω ϑ ϕ ϵ ← → ↔ ↠ ⇐ ⇒ ⇔ ∀ ∃ − √ ∧ ∨ ≠ ≡ ≤ ≥ ⋅ ⌈ ⌉ ⌊ ⌋

Special Commands

/**/Start a new line. A new line may also be started by putting the ⇔, ⇒, etc., to the very beginning of the line. In problem modes that do not support them, put =, >, etc., to the very beginning of the line.
/* two to the `n` is `2^n` */Write a comment and start a new line. Passages surrounded by grave accent characters will be shown as mathematics.
assume x != 1 /\ y^2 < sin x;Restrict the range of variables. Any comparisons and propositional operators may be used in the condition. One may use enda instead of ;. Works in the arithmetic and draw function modes, and almost all problem modes that support logical reasoning chains. Unless otherwise stated, this must be next to the problem mode keyword.