This is the Metamath-lamp Guide repository. If you just want to read the guide, please view the Metamath-lamp Guide site instead.

Metamath-lamp ("Lite Assistant for Metamath) is a proof assistant for creating formal mathematical proofs in the Metamath system. Unlike most other Metamath proof systems (such as mmj2 or original metamath-exe), users can use this proof assistant without installing anything; you can simply run it directly using your web browser.

docs/index.md#metamath-lamp-guide) repository.

The Metamath-lamp Guide is a guide to help you learn more about how to use the Metamath-lamp tool. This guide was primarily authored by David A. Wheeler,

You can use the Metamath-lamp proof assistant now by going to the Metamath-lamp web site.

You can see and contribute to the Metamath-lamp code by going to the Metamath-lamp repository.

Here's a short video demo (without sound).

Here's a simple screenshot of metamath-lamp in action.

Most of the contents of this guide are in the docs/ directory, especially docs/index.md. So if you need to edit something in the guide, that's probably where you should look first.

The contents are in markdown format. We aim to have portable markdown where practical. Proposed changes must pass our markdownlint checker.

You may use, modify, and share this guide under the terms of either the MIT license or the Creative Commons Attribution 4.0 International (CC-BY-4.0) license.

In short, this guide is licensed using the SPDX license expression:

SPDX-License-Identifier: (MIT OR CC-BY-4.0)