The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

The Coq proof of the Odd Order theorem (
http://www.msr-inria.fr/news/the-formalization-of-the-odd-order-theorem-has-been-completed-the-20-septembre-2012/
) closely follows the reference books on the topic. See the section
"Mathematical Sources" at page 5 of
http://hal.inria.fr/hal-00816699/en for detailed explanations of the
material used, and references to the less advanced textbooks used as a
reference for the preliminary parts (finite group theory, Galois
theory, character theory).


On Wed, Aug 13, 2014 at 9:01 PM, Hugo Carvalho 
<hugoccomp AT gmail.com>
 wrote:
> I'm curious to know if there have been efforts towards a full formalization
> of any textbook. I do know of the few books that have accompanying Coq code
> (Software Foundations, CPDT, Coq'Art). but i'm more interested in knowing if
> there is a textbook that was given a formalization after-the-fact (but then
> again, a textbook written from the ground-up with formalization in mind is
> also an interesting project, even if for different reasons).
>
> It seems to me that, outside of "pure Computer Science" topics (such as
> programming, languages, algorithms), the most adequate topic for such a
> textbook would be math; logic and discrete math, specially, but other math
> topics also seem plausible.
>
> Does the Club know of any pointers in this area?