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 <https://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.
--
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 on the web visit
https://groups.google.com/d/msgid/metamath/367f880c-4607-d5b1-68a7-9673751d655f%40panix.com.
