# 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.