digama0/mm0
View on GitHub ↗ ★ 422 Lean
Metamath Zero specification language
14 mentions on Hacker News by 7 people: 1 story, 13 comments · first 2019-10-26 · latest 2026-07-30
20082026
-
…Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0 How do other proof systems compare? Some bug counts: https://tristan.st/blog/in_search_of_falsehood
comment by 7373737373 · 2026-07-30 · in Are We Stuck with Lean? -
…but I've fallen down the proof rabbit hole so I am curious to see how far it could be pushed. [0] https://github.com/digama0/mm0
comment by smj-edison · 2026-07-26 · in Memory safety absolutists -
…which is what reminded me of it. Just thought I'd point to some additional interesting work :) [1] https://github.com/digama0/mm0
comment by smj-edison · 2026-07-06 · in Dungeon Proof Crawler: learn how to write proofs with RPG -
▲ 2
Metamath Cstory by smj-edison · 2026-04-10 · 0 comments
-
…its kernel design has a similar focus on simplicity while cleaning up a lot of metamath's cruft: https://github.com/digama0/mm0 EDIT: and feel free to ask any questions about mm0, I don't know a ton about it yet but I have researched it a…
comment by smj-edison · 2026-04-04 · in Automatic Textbook Formalization -
…the currently best attempt to achieve an unambiguous and secure language seems to be Metamath Zero: https://github.com/digama0/mm0
comment by 7373737373 · 2025-07-30 · in The Math Is Haunted -
Along similar lines, Mario Carneiro wrote a formalisation of a subset of x86 in MetaMath Zero ( https://github.com/digama0/mm0/blob/master/examples/x86.mm0 ) with the ultimate goal of proving that the MetaMath Zero verifier itself is…
comment by Smaug123 · 2024-02-16 · in Is something bugging you? -
…and the same $a statement being used for definitions. I have some hopes for Metamath Zero ( https://github.com/digama0/mm0 ), which is a related system which may be able to fix this. I think this idea is rather synergistic with proof…
comment by 7373737373 · 2023-11-27 · in $10M AI Mathematical Olympiad Prize -
…that are hard for normal people to appreciate, though there is some work on it, including MM0. [0]: https://github.com/digama0/mm0
comment by raphlinus · 2021-08-11 · in Kind: A Modern Proof Language -
…for MM0, down to the hardware, to build a strong trust base on which to build verifiers. [1]: https://github.com/digama0/mm0
comment by infogulch · 2021-04-30 · in Category theory is a universal modeling language -
…of a compact proof can be performed in linear time (!) if the proof is structured correctly. -- https://github.com/digama0/mm0 The fact that proof checking can take linear time (though not proof-finding), and the fact that it incorporates…
comment by infogulch · 2021-01-19 · in The State of State Machines -
…of first-order logic that we can agree on. [1]: Yes, I think this is possible. [2] [2]: https://github.com/digama0/mm0#introduction
comment by infogulch · 2020-05-16 · in Weakening Cycles So That Turing Can Halt -
The fast proof checker I talk about is mm0-c: https://github.com/digama0/mm0/tree/master/mm0-c . It is (deliberately) bare bones, and I'm planning on formalizing approximately the assembly that you get from running that through gcc. There…
comment by digama0 · 2019-10-26 · in Metamath Zero, a bootstrapping theorem prover -
FYI, the current publicly-available code for Metamath Zero is here: https://github.com/digama0/mm0
comment by dwheeler · 2019-10-26 · in Metamath Zero, a bootstrapping theorem prover