A tiny language and checker for theorems and proofs in abstract mathematics

Public Library0.198.20210807-4updated 8 months ago750.23 KB
wapm install liftm/metamath

Need help using WAPM?

chevron_rightGet started here




  • Readme.md



Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. This site has a collection of web pages generated from those proofs and lets you see mathematics developed in complete detail from first principles, with absolute rigor. Hopefully it will amuse you, amaze you, and possibly enlighten you in its own special way.

Metamath on WAPM

This metamath has been slightly patched to be able to run on WASI. Most notably, the ability to execute shell commands has been removed. It only contains the metamath main executable, but no additional .mm databases. set.mm has to be acquired manually from github or metamath.org.

You can try running it on webassembly.sh:

$ curl https://raw.githubusercontent.com/metamath/set.mm/d3dc8f9545186d55b90dd8f4d89ff8e2ec2a3b93/set.mm -o set.mm
metamath "read set.mm" "verify proof *" exit
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> read set.mm
Reading source file "set.mm"... 42913743 bytes
42913743 bytes were read into the source buffer.
The source has 201512 statements; 2673 are $a and 39622 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> verify proof *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
All proofs in the database were verified in 17.59 s.
MM> exit

(If you're using a browser plugin to block third-party XHR like uMatrix, make sure to let curl through, or else it will fail silently.)

<1klast week

Latest version


Latest updated

8 months ago

Unpackaged size

750.23 KB




  • liftm avatarliftm

Run it in the browser