[Top][All Lists]
[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)