Skip to content

All

    Repositories list

    • set.mm

      Public
      Metamath source file for logic and set theory
      HTML
      Other
      10833612813Updated Sep 13, 2026Sep 13, 2026
    • Metamath program - source code for the Metamath executable
      C
      GNU General Public License v2.0
      31107426Updated Sep 6, 2026Sep 6, 2026
    • Redirect lamp.metamath.org to Igor's page
      HTML
      Creative Commons Zero v1.0 Universal
      0000Updated Aug 19, 2026Aug 19, 2026
    • 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
      13732Updated Nov 14, 2025Nov 14, 2025
    • symbols

      Public
      Images for math symbols from the Metamath project (released to public domain)
      HTML
      Creative Commons Zero v1.0 Universal
      1300Updated Oct 5, 2025Oct 5, 2025
    • Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
      Rust
      Apache License 2.0
      12452011Updated May 7, 2025May 7, 2025
    • Guide on how to use the metamath-lamp proof assistant
      HTML
      MIT License
      1611Updated Jan 13, 2025Jan 13, 2025
    • 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…
      Shell
      MIT License
      3120Updated Jun 14, 2024Jun 14, 2024
    • Source of metamath book
      TeX
      Creative Commons Zero v1.0 Universal
      2057162Updated Dec 22, 2023Dec 22, 2023
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.