The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

A while ago I posted the beginnings of a tutorial of Coq for mathematics, at http://people.debian.org/~schepler/coqtut.pdf or http://people.debian.org/~schepler/coqtut.v.html .  I didn't get very far on the project, but it should hopefully be a gentle introduction to the general flow of how you do proofs in Coq.  Then from there you could start looking at use of typeclasses for encoding algebraic varieties which is what I'd recommend.  (For the latter, "Typeclasses for Mathematics" I think is the title of a good introduction for how that would work.)

-- 

Daniel Schepler

On Tue, Jan 14, 2014 at 12:29 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

Wow, thanks all for your answers. This amount of code should keep me
busy for a while. I hope I can understand the Coq used in these
implementations.

---
Ömer Sinan Ağacan
http://osa1.net

2014/1/14 Vladimir Voevodsky <vladimir AT ias.edu>:

>
> On Jan 14, 2014, at 3:18 PM, Daniil Frumin wrote:
>
>> Hi,
>>
>> There are many examples of proof of the specific theorems/properties
>> on the internet: everything from blogposts to Coq contributions that
>> Harley has linked.
>>
>> However, there are also bigger projects, like Math Classes [1], which
>> aim is to develop interfaces (based on Coq's typeclasses) for many
>> algebraic gadgets.
>>
>> Recently, Vladimir Voevodsky has published his paper [2] on his work
>> in the formalization of mathematics. I haven't read it yet, but I
>> guess it deals with Univalence, HoTT and other things I am clueless
>> about.
>>
>> I myself tried to formalize basic category theory [3] and I've got to
>> say it is going slower than I want and it is harder than I initially
>> anticipated.
>>
>> [1] http://math-classes.org
>> [2] http://arxiv.org/abs/1401.0053
>> [2] http://repos.covariant.me/browse?r=cat;a=tree
>
>
> There is a conceptually correct formalization of the basics of basic category theory here:
>
> https://github.com/benediktahrens/rezk_completion
>
> with the accompanying paper here:
>
> http://arxiv.org/abs/1303.0584
>
>
> Vladimir.
>
>