Metamath is famous! Tau Day famous that is

[Jim Kingdon]

This year's State of the Tau includes the following item:

"Aleksandr Alekseevich Adamov (who made the Russian translation of The Tau Manifesto) passed along a link to a formalized proof that τ = 2π"

from tauday.com/state-of-the-tau

and it links to https://us.metamath.org/mpeuni/taupi.html

If you follow the definitions you will see that tau is defined to be the smallest positive real whose cosine is one and pi is defined to be the smallest positive real whose sine is zero, which perhaps clarifies why this is a proof rather than a definition.