Talk:Mizar (software)

Need more simple examples

It would be good to add also examples that check simple relations, in particular,

2>1
x^2=x*x

Explain this to me on a simple example; the difficult example I will be able to do on my own - Israel Gelfand, 1994, http://israelmgelfand.com/edu_work.html

The guide for choice of the libraries seems to be absent. It could be just a script that adds and removes libraries one by one, checking, weather the number of non-accepted lines increases or reduces. But I cannot find such a script at their homepage. What should be a keyword for such a search?

Dmitrii Kouznetsov 05:23, 29 January 2010 (UTC)
P.S. the { {subpages} } is not accepted...

Disambig?

Mizar is also the name of a star, ζ Ursae Majoris. Peter Jackson 14:28, 29 January 2010 (UTC)

Yes, now is better. Thank you! Dmitrii Kouznetsov 04:31, 31 January 2010 (UTC)

An unclear sentence

I am not sure what this means: "the readers of the already existing programs could be used". That all existing libraries are loaded? --Peter Schmitt 11:00, 2 February 2010 (UTC)