Re: [isabelle] wikipedia entry



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.