私たちは、数学を「単なる記号列を変形していくゲーム」とみなします。それを機械に行わせるべく、ルールを決めます。
数学の現場(大学の数学科)で使われる表現を、なるべくそのまま使用できるようにします。

ルールは完全・厳密でなくても機械化できればOKと考えます。また、一部のルールは未完のまま放置されています。
web上でクリックすると出てくるものを注釈と言います。クイズなんかもできます。今日は？