AW: [mizar] where do people check for the MML library?

["Koch, Sebastian" <skoch02@students.uni-mainz.de>]

Hello Brando,

and welcome to the Mizar community. Always nice to see someone new.

If you want to prove trivial facts, I would recommand to take some of the foundational articles (see [1], for example XBOOLE_1 or RELAT_1 or FUNCT_1), copy the abs files into your local directory, try to compile it and then try to prove the statements. Since you also have the miz file with the proofs available, you can always get inspiration from the MML proof in case you get stuck.

I wouldn't directly go for definitions (which need proofs themselves, see appendix of [2]) but start with theorem proving.

From my experience, the fastest way to learn Mizar is to read articles and write a new one yourself. You can start with [1] to look for proofs of statements you know and see how they are handled in Mizar, the HTML version of articles [3], which are linked to in [1], are really nice to read (you can click on "proof"). You can also grab a copy of Walter Rudin's "Principles of Mathematical Analysis" from your local math lib or the Internet and read up with [4] where some basic analysis theorems are in the MML. As you will see, a couple of theorems don't seem to be in the MML yet, so if you want to get active I would be happy to write you an abstract with some proof skeletons to work with. Just tell me so.

Oh, and I have also a personal style guide [5] for writing articles, if you are interested.

Best regards

Sebastian Koch

[1] https://math.stackexchange.com/questions/2806592/getting-to-know-the-mizar-mathematical-library/2806593#2806593

[2] http://jfr.cib.unibo.it/article/view/1980/1356

[3] http://mizar.org/version/current/html/

[4] https://en.wikibooks.org/wiki/Mizar_Commentary_on_Walter_Rudin%27s_Principles_of_Mathematical_Analysis

[5] http://wiki.mizar.org/twiki/bin/view/Mizar/SebastiansStyleGuide

---

Von: owner-mizar-forum@mizar.uwb.edu.pl <owner-mizar-forum@mizar.uwb.edu.pl> im Auftrag von Miranda, Brando <miranda9@illinois.edu>
Gesendet: Freitag, 30. November 2018 00:31:06
An: mizar-forum@mizar.uwb.edu.pl
Betreff: Re: [mizar] where do people check for the MML library?

 

Hi Freek,

Thanks for the response.

I was hoping to learn the syntax by proving trial stuff, like in Coq, its helpful to even define natural numbers myself and define and prove properties about them, like n+m = m + n and other simple facts using even induction.

is that possible in Mizar? Or is that a bad way to go about it?

I will read through it but I feel things don’t stick if I don’t actively do stuff.

I am happy to write something up but I’d need to know what are the common practices, or the “Mizar way to code”.

Regards, Brando

> On Nov 29, 2018, at 5:25 PM, Freek Wiedijk <freek@cs.ru.nl> wrote:
>
> Dear Brando,
>
>> Interesting, so is that not the standard way to learn Mizar?
>
> I don't know what the best way to learn Mizar is :-)
>
> As for the "tutorial", what I would do if I were you is
> just read through it, and not really enter the specific code
> fragments into the system and ignore the exercises for now
> (as I wrote, they are outdated).  But hopefully the text
> will still help you understand the system a bit better.
>
> And if you are into some interesting times, you _could_
> try to update the "tutorial" to make it up to date with
> respect to the current state of the system :-)  But of
> course, as Mizar is a moving target, that will soon be out
> of date again.
>
> Freek