The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

For example here:

https://github.com/vladimirias/Foundations/blob/master/hlevel2/algebra1b.v

Vladimir.


On Jan 14, 2014, at 2:57 PM, Ömer Sinan Ağacan wrote:

> Hi all,
> 
> I finished reading Software Foundations(and solving exercises in it,
> although not all of them) few months ago but never used Coq since
> then. Now I want to use it for something interesting and I was
> wondering how useful is it for something other than programming
> language related fields.
> 
> For example, I'm taking abstract algebra class this semester(I'm not a
> math major -- I'm taking the class just for the fun of it) and I'd
> like to give some proofs about groups and some other abstractions we
> study in the class -- but I have no idea where to start.
> 
> So I mainly want to ask two things:
> 
> 1) How useful is Coq for theorems in fields other than programming
> languages related ones? For example, abstract algebra or number theory
> stuff.
> 2) Can you give me some pointers on where can I see such theorems proven in 
> Coq?
> 
> 
> Thanks,
> 
> 
> ---
> Ömer Sinan Ağacan
> http://osa1.net