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.
1 comment:
I (and other people, apparently) want to see Euler's Identity in Metamath. (Who doesn't like a rigorous proof?)
Megill noted to me in one or two emails that it is hard to prove that π is even real or complex--much less that π is between 3 and 4 like e is shown to be between 2 and 3--without derivatives or analytical functions (or some new form of proof), whether it's defined in the current form or as a series. Those, of course, would need new theorems and definitions that simply don't exist in Metamath (yet).
I think by the time we get to use π, set.mm will be 6 to 7 megabytes big--I doubt proofs of the necessary calculus theorems will be small and cuddly. For now, I hope the theorems I've sent Megill so far bring us a bit closer to π nirvana. :)
Post a Comment