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.

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.................................…

Nonlinear Mathematics Example

An experimental toolkit of metamath based on mmj2

Principia: Metamath-like Logician Language

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

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.

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

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