# 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 ist.tugraz.at
Institute for Software Technology Tel: +43-(0)316/873-5728
University of Technology Fax: +43-(0)316/873-5706
Graz, Austria Home: www.ist.tugraz.at/neuper
------------------------------------------------------------------------
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...
`
Alex

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