Looks like Terrence Tao is planning [1] to follow in the footsteps of Mario Carneiro [2] and formalize the Prime Number Theorem.
More seriously, it is really nice to see people getting excited about formalization. I figure this can only be a good thing. [1] https://mathstodon.xyz/@tao/111847680248482955 [2] https://us.metamath.org/mpeuni/pnt.html -- 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/8102B940-2AD8-4D32-9C26-42FD3ECDB73E%40panix.com.
