Metamath has a definition of π, but it's unused. For all the importance of π in math, the Metamath database contains exactly zero theorems that make use of it.
I started to work on a little something and quickly discovered the reason for this. Metamath defines π as the smallest positive zero of the sine function, but as yet it has no proof that any such number exists!
In a way this reflects well on Metamath. I wanted to prove something, but my reasoning depended on hidden assumptions. Working in Metamath very quickly revealed those assumptions and guided me to an understanding of exactly what they were. You learn by doing.