Skip to content

Guide on how to use the matamath-lamp proof assistant

License

Notifications You must be signed in to change notification settings

expln/lamp-guide

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Metamath-lamp Guide

This is the Metamath-lamp Guide Source markdown repository. If you just want to read the guide, please view the Metamath-lamp Guide site instead. This guide was primarily authored by David A. Wheeler.

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.

You can use the Metamath-lamp proof assistant now by going to the Metamath-lamp application page. If you want to view its source, file issues, or propose changes, see the Metamath-lamp source code repository

You can see the Metamath-lamp Guide markdown file here.

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

Screenshot

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

Screenshot of metamath-lamp showing 2 + 2 = 4

Contents

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.

License

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)

About

Guide on how to use the matamath-lamp proof assistant

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • HTML 92.5%
  • Makefile 7.5%