Re: [isabelle] wikipedia entry

Hi Alexander,

thanks for definitely improving wikipedias article on Isabelle !
The proof "sqrt 2 /= a / b" is actually one of those proofs, non-experts most likely have seen already in a non-computerized variant.

The other suggestion,
# human readable representation of mathematical knowledge, e.g. introducing [[integer]]s based on [[natural number]]s:
    definition intrel :: "((nat × nat) × (nat × nat)) set" where
    [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u + y }"
with examples even for non-mathematicians: ...

would better be included into a more general article like "Interactice theorem proving". Or even better would be a new article "Computer Theorem Proving" (a term already suggested by John Harrison).

Cheers, Walther

Walther Neuper                          Mailto: neuper at
Institute for Software Technology          Tel: +43-(0)316/873-5728
University of Technology                   Fax: +43-(0)316/873-5706
Graz, Austria                             Home:

Alexander Krauss wrote:
Hi Walther,

from time to time having discussions with "pure mathematicians" (i.e.
mathematicians who don't take computers serious beyond LaTeX) about
computer theorem proving (CTP), I would welcome wikipedias entry on
Isabelle supporting arguments like these:

Good point. We actually had this discussion internally last week, and the entry can certainly be improved. I just replaced the strange proof example by an Isar proof that the sqrt of 2 is not rational. I think this is the same direction as what you had in mind...

btw, editing wikipedia is really as easy as clicking "edit", so if anyone has relevant things to write, go ahead. In particular, some major applications should be mentioned...


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.