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.
On Monday, March 9, 2026 at 1:03:50 PM UTC-6 David A. Wheeler wrote:
>
>
> > On Mar 9, 2026, at 1:10 PM, 'Alexander van der Vekens' via Metamath <
> [email protected]> 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
>
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/42dad5ba-d108-454a-a775-30f4d04d9d21n%40googlegroups.com.
