The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I am an amateur mathematician which discovered a new subfield of general 
topology (I call my theory "Algebraic General Topology").

I've written a draft book with my theory:
http://www.mathematics21.org/binaries/volume-1.pdf

Now I am busy with checking it for errors before final submitting my work to 
a publisher.

If I don't notice some error while checking for errors and my book will be 
published with an error, then it may be probably a trouble to produce second 
and further editions as editions of printed books are "set in stone". A 
similar situation applies if I prove a conjecture from my book, add some new 
theorem, or generalize some theorem in my book.

On the other hand, if I formalize my research, then we can update the code as 
often as we want (probably even using a version management software such as 
SVN or Git).

Well, also CoC allows to write formulas (such as category theory equalities) 
shorter than we use in informal math, introducing fewer variables, as type 
inference works. One other advantage.

Saying that, I have not yet finally decided whether to invest my time in 
formalization.

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