I'm not sure that C-CoRN really has a proof of Leibnitz's series for pi.
The problem is the C-CoRN has two defintions of pi.
"pi" is defined by Leibnitz's series.
"Pi" is defined by a different sequence.
However, these two constants are never shown to be equal. "Pi" is used in
the rest of the development, while "pi" is never touched again (as far as
I know).
Proving that Leibnitz's series converges and defining the limit to have
the name "pi" is probably not in the spirit of the task.
On Fri, 9 Jan 2009, Laurent Théry wrote:
Freek (Wiedijk) maintains a page of the 100 theorem that has been formalized
in
different provers.
http://www.cs.ru.nl/~freek/100
Specific pages already exists for several provers.
As a 2009 good deed, I engage myself with freek to set-up such a page for
Coq.
Fortunately, I discover that such page already exists, it just needs to be
updated:
http://logical.saclay.inria.fr/cocorico/Top100MathematicalTheoremsInCoq
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
_______________________________________________
C-CoRN mailing list
[email protected]
http://mailman.science.ru.nl/mailman/listinfo/c-corn
