More than 50.000 theorems in set.mm

[Alexander van der Vekens]

I was waiting for it for months, but then I missed the precice date of this magnificent event: we exceeded the limit of 50.000 theorems in set.mm recently. Unfortunately, I do not know who was the contributor of the 50.000th theorem.

Maybe someone could add this news to the web page https://us.metamath.org/mpeuni/mmrecent.html - it has not been updated for a long time... 

[David A. Wheeler]

> On Mar 9, 2026, at 1:10 PM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>
> I was waiting for it for months, but then I missed the precice date of this magnificent event: we exceeded the limit of 50.000 theorems in set.mm recently.

That *is* impressive! Thank you, whoever you were!

> Unfortunately, I do not know who was the contributor of the 50.000th theorem.

Every change is listed in the git log, so that is something that *could* be determined.
Someone would need to write a script to figure that out
(e.g., identify every new theorem not counting renames, along with date/time & person).
Writing that script sounds like a good job for an AI :-).

> Maybe someone could add this news to the web page https://us.metamath.org/mpeuni/mmrecent.html - it has not been updated for a long time...

Sounds good. We *can* update that, we just haven't yet.
Probably time to do so :-).

--- David A. Wheeler

[Eric Schmidt]

Loading a database into metamath-exe prints the number of $a and $p statements in it. When I do this with the latest 'develop' commit (22ae5646a8949ef1d08fb5dd9d0aca735af3f16f), I get 

       The source has 246644 statements; 2977 are $a and 47069 are $p.

So while the total number of $a and $p statements exceeds 50000, we haven't actually reached 50000 theorems yet.

[Alexander van der Vekens]

erics...@gmail.com schrieb am Dienstag, 10. März 2026 um 01:39:54 UTC+1:

Loading a database into metamath-exe prints the number of $a and $p statements in it. When I do this with the latest 'develop' commit (22ae5646a8949ef1d08fb5dd9d0aca735af3f16f), I get 

       The source has 246644 statements; 2977 are $a and 47069 are $p.

So while the total number of $a and $p statements exceeds 50000, we haven't actually reached 50000 theorems yet.

You are right, so we have more than 50.000 axioms, definitions and theorems.