Re: [mizar] Good news from a mathematician

[Freek Wiedijk <freek@cs.kun.nl>]

Hi Piotr,

>How HOL can help more with the optimization problems than
>Mizar?  I do not know.  Does anybody?

I do not know how it helps with these optimization problems
of Hales _specifically,_ but I can give some general
comments.

In HOL you can automate things if you know how to prove
something algorithmically.  For instance, in HOL you can
write an ML function called INT_NORMALIZE_CONV (of ML type
"term -> thm") and then it works something like this:

#INT_NORMALIZE_CONV `(x + y) pow 2`;;
it : thm = |- (x + y) pow 2 = x pow 2 + &2 * x * y + y pow 2
#

Now it's not unthinkable that in Mizar you'd have a
"requirement" that gives you this, but the point of such a
"conv" thing is

(a) it is a first class citizen of the system
    (it's something like a term or a formula, not something "special")

and

(b) the user can write as many of them as he likes/needs
    (it's not something that only the developer of the system can do)

So Hales might have this kind of automation for doing linear
programming proofs, maybe.  How would he go about that in
Mizar?

Freek