metamath

Meta mathematics. Symbolic functions and derivatives.

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

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 your web browser).

Guide on how to use the metamath-lamp proof assistant

A Metamath Zero Verifier Written in Zig

A Metamath Zero kernel for Trivial

The AI mathematician that breaks conjectures before proving them, discharges every step inside a proof assistant, and hands you a proof you can check yourself.

An experimental toolkit of metamath based on mmj2

Principia: Metamath-like Logician Language

Nonlinear Mathematics Example

A project based on metamath.org ; personal new mathematics foundational & other tertium datur openscience theories by Evgeniy Grigoriewitch Phfilippowvv Angarskiy AKA https://beacons.ai/krichuvka vk.com/egphilippov https://linkedin.com/in/egphilippov as of Sunday, February 13 ante de Christ and further since that.................................…

Axiom provenance for Lean 4 and Metamath — which step introduced an axiom, and whether the theorem statement required it Website: https://f-keys.com/gonzalgo/

Metamath proof verifier

Create a Generative Pretrained Transformer model for Metamath to generate metamath assertions

This repository contains code that is referenced in my Master thesis. For the most part, it includes formal proofs that are checkable by proof assistants.

WIP Metamath proof verifier written in x86 assembly

Verifier for Metamath proof databases written in Julia

A browser userscript to enhance metamath.org proof pages

Metamath Claim Explorer