The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Hi all,

Once I attempted to learn and use Coq. Then I decided not to continue with 
Coq for reasons in my pre-previous email to this mailing list.

As for now, I've forgotten much of it and would need learn it anew.

With a solution offered by Olivier Uanelineur, the reason why I stopped to 
use Coq disappeared.

So I am now again faced with the decision: Should I use Coq?

I'd like to formalize poset/lattice theory with Coq and afterward to 
formalize my theory.

I've recently put my entire theory into one 216 A4 pages book. Now I am busy 
with checking my book for errors. In any case I need to finish my (manual) 
checking for errors in the book and settle it with a publisher. (And I find 
many little errors while checking it.)

Is it worth to formalize my book in Coq afterward?

I now have no definite purpose in this life. It may be more useful for the 
community if I continue my (informal) research and write a second book (or 
supplementary articles). But should I do what is good for the community? 
http://portonmath.wordpress.com/2011/05/03/my-math-research-motivation/ - I 
have no strong motivation to do this. (Well formalizing posets in Coq may be 
also considered useful for the community.) I may probably just play. Would 
formalizing in Coq be an interesting game? Or should I refuse to follow 
interest and attempt to do something useful (even despite I feel nothing I 
can do would be useful for God)?

Sorry for offtopical purposing philosophy in this mailing list.

More info about my pure math research:
http://www.mathematics21.org/algebraic-general-topology.html

PDF of my book while its copyright is not yet transferred to a publisher:
http://www.mathematics21.org/binaries/volume-1.pdf

And BTW the list of errors I found for now (in order to see whether such a 
quantity of errors is a strong argument to formalize to ensure no errors):
http://www.mathematics21.org/binaries/volume-1-changes.pdf

-- 
Victor Porton - http://portonvictor.org