The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

I believe the first formalization of a math book was that of Landau's 
"Grundlagen der Analysis" in Automath (a predecessor of Coq), by van Benthem 
Jutting in the 1970s. His thesis can be found here: 
http://www.win.tue.nl/automath/archive/pdf/aut046.pdf . There appear to be 
translations from Automath code to Coq, according to the abstract of this 
paper by Chad Brown: 
http://www.ps.uni-saarland.de/Publications/documents/Brown2011b.pdf .

Dimitri





On 14 Aug 2014, at 5:06 , Benjamin C. Pierce 
<bcpierce AT cis.upenn.edu>
 wrote:

>> 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)
> 
> Software Foundations goes some distance in that direction, but dealing with 
> variable binding in a way that doesn’t get too heavy for a book intended 
> for teaching is a significant challenge.  By stopping at simply typed 
> systems, I was able to use the trick of only considering substitution of 
> closed terms, which streamlines things quite a bit.  
> 
>     - Benjamin
> 
> 
>> 
>> 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).
>> 
>> 
>> 
>> 2014-08-13 16:35 GMT-03:00 Harley D. Eades III 
>> <harley.eades AT gmail.com>:
>> Hi, Hugo.
>> 
>> The Homotopy Type Theory book is a nice example.  It can be found here:
>> 
>> http://homotopytypetheory.org/book/
>> 
>> A large portion of the book was formalized as it was written.
>> 
>> Very best,
>> .\ Harley
>> 
>> On Aug 13, 2014, at 3: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?
>> 
>> 
>