Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] wikipedia entry

Email Gateway (Aug 18 2022 at 13:58):

From: Alexander Krauss <krauss@in.tum.de>
Hi Walther,

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

Email Gateway (Aug 18 2022 at 14:01):

From: Walther Neuper <neuper@ist.tugraz.at>
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

Email Gateway (Aug 18 2022 at 14:03):

From: Walther Neuper <neuper@ist.tugraz.at>
Dear list members,

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:

CTP represents mathematical knowledge in (almost) traditional notation

CTP, in particular Isar, represents proofs in (almost) traditional

notation
... both representations can be read by humans as well as be interpreted
by machines, and thus CTP is a straight-forward continuation in the
tradition of pure mathematics (... might well be weakened ;-)

With respect to the standard reader of wikipedia, doesn't the present
article emphasize technicalities too much ? Wouldn't be information more
appropriate like:

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:
((3, 1), (4, 2)) | 3 + 2 = 1 + 4 ,
((3, 1), (5, 3)) | 3 + 3 = 1 + 5 ,
((3, 1), (6, 4)) | 3 + 4 = 1 + 6 , ...
i.e. (3, 1) \equiv (4, 2) \equiv (5, 3) \equiv (6, 4) \equiv ...
where this [[equivalence class]] is written as [[integer]] "-2"

representation of proofs: Shouldn't the outdated "programing style"

proof be replaced by an example for an Isar proof (while there might be
better examples than the one addressed by the link "declarative proof
style") ?

Is somebody out there, who is unsatisfied with the present article _and_
expert enough to make an acknowledged revision ?

Walther

Last updated: Apr 25 2024 at 16:19 UTC