Advent of Metamath 2024

A tactics-based Metamath proof language

Metamath Blueprints

Layout is a rust library and a tool that renders Graphviz dot files.

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using …

A verified implementation of a metamath proof checker

A Visual Studio extension and LSP server for Metamath

Lightning-fast and Powerful Code Editor written in Rust

Metamath web server

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.

A quick experiment to demonstrate Metamath formula parsing, where the grammar is embedded in a few additional 'syntax axioms'.

A place where Druid widgets come to mature before moving to the Druid repo.

A data-first Rust-native UI design toolkit.

A self-hosted browser-based cloud IDE, updated from Codiad IDE

The osTicket open source ticketing system official project repository, for versions 1.8 and later

A metamath plugin for Eclipse

Metamath source file for logic and set theory

Metamath database for dependent type theory

A Metamath library for the Q0 logic