GitXplorerGitXplorer
d

mmverify.py

public
36 stars
10 forks
2 issues

Commits

List of commits on branch master.
Verified
ee80f30ea8e2492cc4cc5e9b5add05ce6ea00932

Merge pull request #25 from drvdw/fix/nonactive-hypotheses

ddavid-a-wheeler committed 9 months ago
Unverified
cb84471d9fa8ea7b93d59aa401e4a34ac9b52075

This commit addresses an issue where hypotheses are erroneously active outside of their intended scope.

committed 9 months ago
Verified
45a736383a36744b6948a1e61bdec8986594348a

Merge pull request #23 from zhengying-liu/master

ttirix committed 10 months ago
Unverified
4d185c683eb1ca134ac03efae01fe0d48160da9d

Fix Fhyp type

zzhengying-liu committed 10 months ago
Verified
865e742c87edb556fea3c5a73d2e513632948548

Merge pull request #21 from david-a-wheeler/parallel_testing

ddavid-a-wheeler committed 2 years ago
Unverified
7501f5b9d35c41129bfb72578082ee56f7282698

Parallelize tests

ddavid-a-wheeler committed 2 years ago

README

The README file for this repository.

mmverify.py

This is a Metamath verifier written in Python, originally by Raph Levien.

Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. The set of proved theorems using Metamath is one of the largest bodies of formalized mathematics. Multiple Metamath verifiers (written in different languages by different people) are used to verify them, reducing the risk that a software defect will lead to an incorrectly verified proof.

For a quick introduction to Metamath and its goals, see the video Metamath Proof Explorer: A Modern Principia Mathematica.

For more information about Metamath, see the Metamath website.

You can also get the (physical) book about Metamath; see: Metamath: A Computer Language for Mathematical Proofs by Norman Megill & David A. Wheeler, 2019, ISBN 9780359702237.

This software is free-libre / open source software (FLOSS) released under the MIT license.