Repositories list

• set.mm

  Public
  Metamath source file for logic and set theory

  HTML

  •

  Other

  •100•296•119•7•Updated Oct 13, 2025Oct 13, 2025

• symbols

  Public
  Images for math symbols from the Metamath project (released to public domain)

  HTML

  •

  Creative Commons Zero v1.0 Universal

  •1•3•0•0•Updated Oct 5, 2025Oct 5, 2025

• metamath-website-seed

  Public
  Starting seed files for metamath public website. The website starts with these and then uses generation scripts to generate other files from the .mm files

  HTML

  •

  Other

  •11•7•2•2•Updated Sep 9, 2025Sep 9, 2025

• metamath-exe

  Public
  Metamath program - source code for the Metamath executable

  C

  •

  GNU General Public License v2.0

  •29•86•37•7•Updated Jul 29, 2025Jul 29, 2025

• metamath-knife

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

  Rust

  •

  Apache License 2.0

  •12•35•19•9•Updated May 7, 2025May 7, 2025

• lamp-guide

  Public
  Guide on how to use the metamath-lamp proof assistant

  mathproofmathematics+ 3proofsformalismmetamath

  HTML

  •

  MIT License

  •1•4•1•1•Updated Jan 13, 2025Jan 13, 2025

• metamath-website-scripts

  Public
  Scripts to set up the metamath website(s) so they're under version control, can be reviewed, and can be rerun. The scripts download the seed files from metamath-website-seed, databases from set.mm, etc.

  Shell

  •

  MIT License

  •3•2•2•0•Updated Jun 14, 2024Jun 14, 2024

• metamath-book

  Public
  Source of metamath book

  TeX

  •

  Creative Commons Zero v1.0 Universal

  •18•51•15•2•Updated Dec 22, 2023Dec 22, 2023