The Coq mailing list

[Daniil Frumin <difrumin AT gmail.com>]

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

Cheers.


On Tue, Jan 14, 2014 at 11:57 PM, Ömer Sinan Ağacan
<omeragacan AT gmail.com>
 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



-- 
Sincerely yours,
-- Daniil