Metamath-rs - a library for processing Metamath databases

A what?

Metamath is a language for expressing formal proofs in mathematics. Metamath makes few assumptions on the underlying logic and is simple enough to support a wide variety of tools. See http://us.metamath.org/#faq.

Metamath-rs can rapidly verify these proofs, providing much stronger confidence that the proof is correct. And we do mean rapid: over 28,000 proofs can be proved in less than a second.

Metamath-rs is the library component of the metamath-knife project, which also contains a standalone command-line application.

• It supports all Metamath proof formats. In particular, Metamath-knife adds support for all Metamath proof formats (uncompressed, compressed, package, or explicit.
• We take extra steps to prevent errors, e.g., we have a CI pipeline (implemented using GitHub actions).
• We remove deprecated constructs, e.g., the deprecated try!(...) has been replaced with the easier-to-read "?" construct.
• We actively work to eliminate compiler warnings. This tends to counter errors, make the code more readable, and improve performance (e.g., by eliminating unnecessary clone() calls).

License

This is licensed under either of

• Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

The SPDX license expression for its license is "(MIT OR Apache-2.0)".

Note that this is exactly the same license as smetamath-rs (SMM3), That is intentional, because we want smetamath-rs (SMM3) to be able to re-incorporate whatever we do if they like.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.