Dear C-Corn developers/users,
I and my students are strongly interested in formalizing constructive
mathematics.
Although we are originally mathematicians and have some experience in
using Coq, dealing with pure mathematics in Coq is new for all of us. So
we are wondering whether the C-Corn project is a good starting point for
us, which we hope strongly.
Currently we are in the phase of thinking of and looking for some well
known and interesting, but hopefully not so difficult mathematical
theorems which we could set as our first target.
We also looked at Freek Wiedijk's "Formalizing 100 Theorems" website,
but we are not sure which parts of the C-Corn library provide a good
base for some of the theorems mentioned there.
We haven't yet checked all the contents of the C-Corn library. So we
will be highly grateful when you can give some hints about or
information of the current state of the library.
Thanks in advance
Gyesik
_______________________________________________
C-CoRN mailing list
[email protected]
http://mailman.science.ru.nl/mailman/listinfo/c-corn
