The Coq mailing list

[Harley Eades <harley.eades AT gmail.com>]

Hi, 

omeragacan AT gmail.com
 writes:

> 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?

Here is some group theory done in Coq:

http://coq.inria.fr/V8.2pl1/contribs/GroupTheory.html

Keep in mind that the theory your professor will use will most likely be
based on classical mathematics, while the proofs you do in Coq will be
constructive by default.  A lot of math can be done constructively, but
the proofs you do in Coq will most likely be a lot different then the
proofs you do in class.  This is not necessarily a bad thing.

Have fun.

.\ Harley


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

-- 
Sent with my mu4e