The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Wed, Aug 13, 2014 at 10:03 PM, Hugo Carvalho 
<hugoccomp AT gmail.com>
 wrote:
> Thanks!
>
> I had heard of the Odd Order Theorem formalization, but always assumed it
> followed a paper (with ad-hoc proofs of elementary statements, taken from
> whatever references as needed), not an actual (pair of) textbook(s). And
> some fairly advanced ones, at that! I'll be sure to check it out. I guess
> i'll also have to give ssreflect tatics a chance... (i don't even know
> anything about them, i'm just scared of change; but come on,
> CPDT/Chlipala-style code just seems so much cleaner (even if i'll never be
> smart enough to reproduce it))
>
> The HOTT book is just delightful, isn't it? I hope we see more books written
> in this collaborative, in-the-open, formalized style. But come on! It's type
> theory, that's, like, the one thing i would expect Coq to excel at
> formalizing! That's cheating! :)
> Altough now i wonder just how difficult would be to formalize Benjamin
> Pierce's "Types and Programming Languages"... (and also wonder if i'll ever
> get around to start reading it seriously)
>
> If anyone cares, here's why i asked this question. I've read somewhere that
> one of the challenges proof assistants face is to be convenient/useful
> enough that they get regularly used by mathematicians, as right now they
> require too much specialized training. My train of thought was simply "Well,
> maybe they can't be used in the day-to-day work, proving cutting-edge
> theorems. But perhaps a few undergraduate textbooks have been formalized,
> showing that it is possible to use a broad range of introductory
> mathematical reasoning within proof assistants?".
> And to clarify, i know you can reason with math in a proof assistant, it's
> kind of the whole point of the ordeal, but i assume that textbooks, in
> addition to explaining whatever their topic might be, also show by example
> how to compose proofs about the subject, in a way that's useful to a
> mathematician for their whole career. So if you show how to replicate the
> usual textbook within a proof assistant, you've shown how to do a fairly
> general amount of math within a proof assistant.
> Of course, this is all quite optimistic. Maybe the usual way of doing math
> just isn't going to convince a computer, and we're going to need a radically
> new kind of way to do it, instead of building blocks that eventually lets us
> do math the old-fashioned way (except in a checked environment).

The Topology contribution might be interesting to look at.  My goal
there was to do some formalization of the basic concepts of an
introductory undergraduate-level course on topology, and I built it up
to the level of formally proving Urysohn's lemma and the Tietze
extension theorem.  It's rather lacking in examples, though.  It's
also not based on any particular textbook (but then again, neither was
my introductory topology course); and it uses the logical progression
rather than a more typical introductory sequence (i.e. it starts with
general topological spaces then specializes to metric spaces and then
to R, rather than starting with R^n and generalizing to metric spaces,
then to topological spaces).
-- 
Daniel Schepler