Re: [mizar] Good news from a mathematician

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

Hi Josef,

>> So Hales might have this kind of automation for doing linear
>> programming proofs, maybe.  How would he go about that in
>> Mizar?
>
>Some time ago, I started writing this (it is not an answer to your 
>question, just some suggestions):
>http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/ComputerAlgebraInMizar

If I understand this correctly you have four options:

- Do nothing
- Have something called "requirements"
- Add a programming language for proof generation to Mizar
  (and present it like it's a generalization of schemes)
- Add a way to call external proof generators to Mizar

Option three is your real proposal, I guess?  But it's not
really clear to me what such a programming language would
look like.

Freek