11. Mizar Proof Advisor

Mizar Proof Advisor is a system trained on MML proofs by data mining techniques. The server is running at http://lipa.ms.mff.cuni.cz/~urban/posdemo.html.

It gets a formula in MML Query constructor format and gives you theorems and definitions, that it evaluates as most promising for proving the formula.

You can have a look at the success hitrates obtained by 10-fold cross-validation at http://lipa.ms.mff.cuni.cz/~urban/hitrate.jpg.

The typical usage in Mizar Mode is to ask for advice on a formula, which you want to prove. Mizar Proof Advisor uses constructor representation, so you have to use Constructor explanations, See section 9. Constructor explanations, for more.

Once you are in the buffer *Constructors list*, use the command C-c C-c (mizar-ask-advisor) to get the advice.

User Option: advisor-limit

The number of hits you want Mizar Proof Advisor to send you.

The default value is 30.

Command: mizar-ask-advisor

Send the contents of the *Constr Explanations* buffer to Mizar Proof Advisor.
Resulting advice is shown in the buffer *Proof Advice*, where normal tag-browsing keyboard bindings can be used to view the suggested references.