XExelxebar·Jul 30, 2026
Yeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm
In Are We Stuck with Lean?metamath
set.mm
HTML2020–2026
metamath / set.mm
set.mm
Metamath source file for logic and set theory
4Distinct people
6Mentions
1Explicit recommenders
338GitHub stars
What to know before exploring
What it is
Metamath source file for logic and set theory
GitHub
Where it is used
No documented product use has been verified yet.
What people are saying
For anyone interested in formal verification, there's this super slick project Metamath Zero [0] by Mario Carneiro that is working to implement a verifier that can verify…
xelxebar used a recommendation phrase. One indexed comment matches. This is a phrase match, not a verdict.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 3:56:07 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year6 dated mentions
Observed mentions: 2020-05-26 19:06:15 UTC to 2026-07-30 15:04:36 UTC.
* An incomplete calendar period is marked with an outlined bar. Its count is not directly comparable with a full period.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2020 | 2020-01-01 00:00:00 UTC | 2021-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2021 | 2021-01-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2022 | 2022-01-01 00:00:00 UTC | 2023-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2023 | 2023-01-01 00:00:00 UTC | 2024-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2024 | 2024-01-01 00:00:00 UTC | 2025-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2025 | 2025-01-01 00:00:00 UTC | 2026-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2026 (partial) | 2026-01-01 00:00:00 UTC | 2027-01-01 00:00:00 UTC | 1 | 0 | 1 |
What Hacker News says
6 sourceshttps://github.com/metamath/set.mm , if you do not object to your theorems being machine-provable.
In Ask HN: Good Online Maths Communities?Correct. The good news that Elements still works otherwise, you just need to add the missing axiom.
But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list just a few of the many examples of proofs that weren't.
Sure, there can be bugs in programs, but there are ways to counter such bugs that give FAR more confidence than can be afforded to humans. Lean's approach is to have a small kernel, and then review the kernel. Metamath is even more serious; the Metamath approach is to have an extremely small language, and then re-implement it many times (so that a bug is unlikely to be reproduced in all implementations). The most pop
Read the rest
ular Metamath database is "set.mm", which uses classical logical logic and ZFC. Every change is verified by 5 different verifiers in 5 different programming languages originally developed by 5 different people:
* metamath.exe aka Cmetamath (the original C verifier by Norman Megill)
* checkmm (a C++ verifier by Eric Schmidt)
* smetamath-rs (smm3) (a Rust verifier by Stefan O'Rear)
* mmj2 (a Java verifier by Mel L. O'Cat and Mario Carneiro)
* mmverify.py (a Python verifier by Raph Levien)
For more on these verifiers, see: https://github.com/metamath/set.mm/blob/develop/verifiers.md
"Here is a list of some of what has been written about this or things we can do:" https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theore...
In Formalizing 100 TheoremsFor anyone interested in formal verification, there's this super slick project Metamath Zero [0] by Mario Carneiro that is working to implement a verifier that can verify itself, compiled binary and all.
As discussed on the project page, Lean is aimed at being ergonomic but at the price of a large (and somewhat buggy) codebase. On the opposite end of the spectrum is Metamath [1] which aims at being the minimum needed for formal verification, but at the cost of extremely pedantic (albeit interesting!) proofs.
Metamath Zero, attempts to find a happier balance by designing a language which is both ergonomic for the proof-writer as well as minimal enough to allow self-verification.
At the moment, the project is still pretty alpha but Mario is both extremely talented and actively developing. That said, if you are someone like me and just want
Read the rest
to dive into the math, definitely check out Metamath [1]. It's library of proofs for standard ZFC foundations, set.mm [2], is seriously impressive. I mean, you can find a proof of the fundamental theorem of calculus and trace it all the way back to axioms if you so please (see theorems ftc1 [3] and ftc2 [4])!
For someone with a background in math, the set.mm [2] database is an absolute blast to rogue around in. It takes some getting used to, but I am starting to prefer set.mm over Wikipedia when applicable.
Anyway, I love this stuff!
[0]:https://3g2upl4pq6kufc4m.onion/html?q=metamath%20zero
[1]:http://us.metamath.org/mm.html
[2]:https://github.com/metamath/set.mm
[3]:http://us.metamath.org/mpeuni/ftc1.html
[4]:http://us.metamath.org/mpeuni/ftc2.html
There's some work on this already, including Holophrasm and work by OpenAI on proof shortening. These efforts are linked from the Metamath wiki:
https://github.com/metamath/set.mm/wiki/Automated-proving
In Symbolic mathematics finally yields to neural networks