Re: [isabelle] wikipedia entry
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