The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

There is an elephant in the room here: you should/could have a look at
the ssreflect library, the math-comp library, and the proof of the
Feit-Thomson theorem for non-pl stuff.

On Tue, Jan 14, 2014 at 9:53 PM, Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 wrote:
> This sounds awesome. I'll start reading that as first thing. Thanks.
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net
>
>
> 2014/1/14 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.
>>> >
>>> >
>>
>>