Hi all.
I'm a former math grad student, and I'm starting to learn Mizar.
My goal is to understand the challenges in computerized proof assistants better.
(I looked at some proof assistants, and it seems Mizar has relatively good features for mathematical abstraction, with Ghilbert maybe a little better but with a tiny library)
So I picked an area of the mathematical space I'm familiar with but with little coverage in Mizar - the Lebesgue measure - and not I'm trying to prove some well-known theorems about it.
I'm having some trouble with writing proofs in Mizar and would be glad if you could help me out.
1. Is this really not covered? AFAICT, the Lebesgue measure only appears in two definitions in the end of MEASURE7. If it is covered, or if anyone else is in the process of formalizing this, I'll pick another area.
2. Is my coding style good? Are there any theorems that would be better represented as clusters? Or some other changes? Also, my proofs seems very long while containing little actual mathematics, is there some kind of optimization I'm missing?
(But the proof of e.g. MEASURE7:Th1 is long as well, so I don't have much hope for any proof involving sequences)
3. Some of the inference chains make the Mizar engine seem "less smart" than others. For instance, the end of the proof of EmptySetMeasureZero. Or algebraic manipulations, such as
A5: c > a;
set b = (a + c) / 2;
a + c > a + a by A5, XREAL_1:6;
then (a + c) / 2 > (a + a) / 2 by XREAL_1:74;
then A6: b > a;
which would be nicer if it had equalities instead of inequalities.
4. I found almost no documentation of the system, especially its semantics. My resources are Freek Wiedijk's tutorial, the Mizar Manual, skimming the PC Mizar book, and a few pages on the TWiki (list of articles, list of error messages). So in many cases, when I have a problem I'm trying all kinds of stuff randomly until one thing works. For example, I don't understand the difference between Real and Element of REAL. As another example, I don't know what the "correctness" stanza of a registration should justify. Are there any more sources to learn about Mizar?
5. I can't find documentation for the smarter tools - MML query, Proof advisor, MoMM. So I don't use them, and this is probably slowing me down. Can you point me to their documentation?
I will appreciate any sort of ideas, response or discussion.
Thanks in advance,