| Author | CCL | MML | Author | CCL | MML | |
|---|---|---|---|---|---|---|
| Grzegorz Bancerek | 19 | 91 | Agnieszka J. Marasik | 1 | 4 | |
| Czeslaw Bylinski | 3 | 36 | Robert Milewski | 8 | 25 | |
| Noboru Endou | 2 | 16 | Adam Naumowicz | 3 | 11 | |
| Adam Grabowski | 4 | 22 | Piotr Rudnicki | 3 | 43 | |
| Ewa Gradzka | 1 | 2 | Yuji Sakai | 1 | 3 | |
| Jaroslaw Gryko | 3 | 6 | Bartlomiej M. Skorulski | 2 | 4 | |
| Artur Kornilowicz | 11 | 45 | Andrzej Trybulec | 3 | 86 | |
| Beata Madras | 1 | 7 | Mariusz Zynel | 2 | 5 |
Can we do formalization of advanced mathematics like that included in regular mathematical monographs in the current proof-checking systems?Especially, in our case, we may ask:
Can we do such formalization in Mizar?Why is the question so important? -- Former formalizations dealt with small and separated mathematical theories chosen often to be easy to formalize. There were, at least two exceptions: Jutting's formalization of Landau's Grundlagen in AUTOMATH and mizaring of Grzegorczyk's Arithmetic in Mizar 2. Both those systems did not required, let me call it, continuous formalization. That means that one may use statements which were not proved, e.g. mathlore. In recent Mizar any articles accepted to the Mizar Mathematical Library has to be a continuation of the Library.
In the MML there was (and still is) a quite big number of articles formalizing beginning of some theory and the theory has no continuation. However, those articles were, mainly, devoted to form the base for more advanced theories. The challenge consists in the fact that against such formalizations the mizaring of the monograph requires much bigger machinery of interrelated concepts and facts, and, then, needs more careful decisions on the way of formalization which may influence later.
Other question was if the MML was enough big to do such formalization.
Publications