isarmathlib-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Isarmathlib-devel] Is it worth to work on IsarMathLib?


From: Slawomir Kolodynski
Subject: Re: [Isarmathlib-devel] Is it worth to work on IsarMathLib?
Date: Sun, 26 Dec 2010 07:25:38 -0800 (PST)

--- On Sat, 12/25/10, Victor Porton <address@hidden> wrote:

> I reason whether it is worth for me to continue to work
> with Isabelle

I really would like to say yes but the truth is it depends on what motivates 
you.

If you are outside of academic environment your work may be treated more 
seriously if it is backed by a formalization. Non-trivial math requires effort 
to be understood (almost a definition of non-trivial) and people are more 
willing to invest that if they know that the stuff is formally correct. 

As you noticed writing formal proofs is difficult and tedious. The very fact 
that you can do that shows than you know mathematics. I bet less than half of 
professional mathematicians are able to formulate their thoughts on the level 
of correctness required by mechanized proof checkers. However, only people who 
did write some formal proofs know about that and those are very few. So I would 
not count on impressing other mathematicians with that skill. 

If you are in academic environment then you have less reasons to work that 
hard. In any case you need to somewhat enjoy writing formal proofs to be able 
to do that for a longer period of time.

> Could we expect that lattices and complete lattices will
> arrive in IsarMathLib in near future even without my help?

No, you would have to do that by yourself.

> Would formalizing it in
> IsarMathLib help me to receive help from other
> mathematicians who would possibly shorten my list of
> conditions? Does it make sense to work in IsarMathLib with
> that purpose?

Probably not. But formalizing gives insight and you would know all there is to 
know about the stuff. If there is any way to simplify it, you would be able to 
do that without help from others. 

slawekk

http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)



      



reply via email to

[Prev in Thread] Current Thread [Next in Thread]