MML Query (home page)

Mizar project
page generated with MMLQT (MML Query Transformation) tool
Mizar home, download
files: abstr, articles,
bin, doc, emacs gabs, fmbibs, gabs (more) semantic MML
Megrez
MML Query (beta)

Template maker
Environment explanation
Mizar TWiki
MML Query server
Megrez services
Journals:
   FM: MetaPRESS, server, proof-read, regeneration
   MM&A (preparation)
Syntax: xml, html
Downloads
Mizar syntax, xml, txt
MML 5.94.1493
- most important facts (other collection) MML links Monographs
Conference MKM2004
Workshop 30 years of Mizar
dydaktyka (e-learning)
Mizar Mathematical Library (version 5.94.1493) includes 1498 articles written by 278 authors and 73460 theorems, 14291 definitions, 912 schemes, 19054 registrations, 10439 symbols. (more statistics, other versions)
New:      monograph: TG Set Theory      authors by # of important facts      environment explanation
decode
MML links:

Latest 30 articles (the query: list of article ordered by historical order reversed select 0-29)
  1. group_24: Semidirect Products of Groups by Alexander M. Nelson (submitted May 27, 2025)
    117 theorems, 9 definitions, no schemes, 17 registrations, authors:Alexander M Nelson, abstract, semantically linked, FM , full article, gab.

  2. polnot_2: Extensions of Languages in Polish Notation by Taneli Huuskonen (submitted May 23, 2025)
    21 theorems, 25 definitions, no schemes, 18 registrations, authors:Taneli Huuskonen, abstract, semantically linked, FM , full article, gab.

  3. newton06: Application of Complex Classes to Number Theory by Rafal Ziobro (submitted May 11, 2025)
    83 theorems, no definitions, no schemes, 99 registrations, authors:Rafal Ziobro, abstract, semantically linked, FM , full article, gab.

  4. gr_free0: Free Product of Groups by Sebastian Koch (submitted April 27, 2025)
    73 theorems, 13 definitions, no schemes, 23 registrations, authors:Sebastian Koch, abstract, semantically linked, FM , full article, gab.

  5. surrealc: Conway's Normal Form in the Mizar System by Karol Pak (submitted April 10, 2025)
    106 theorems, 23 definitions, 1 scheme, 24 registrations, authors:Karol Pak, abstract, semantically linked, FM , full article, gab.

  6. surrealn: Surreal Dyadic and Real Numbers: A Formal Construction by Karol Pak (submitted April 10, 2025)
    80 theorems, 12 definitions, no schemes, 31 registrations, authors:Karol Pak, abstract, semantically linked, FM , full article, gab.

  7. surreals: Surreal Numbers: A Study of Square Roots by Karol Pak (submitted April 10, 2025)
    32 theorems, 9 definitions, no schemes, 9 registrations, authors:Karol Pak, abstract, semantically linked, FM , full article, gab.

  8. field_16: Finite Fields by Christoph Schwarzweller (submitted December 27, 2024)
    73 theorems, 8 definitions, 1 scheme, 50 registrations, authors:Christoph Schwarzweller, abstract, semantically linked, FM , full article, gab.

  9. relset_3: Some Number Relations by Sebastian Koch (submitted December 27, 2024)
    78 theorems, 4 definitions, no schemes, 17 registrations, authors:Sebastian Koch, abstract, semantically linked, FM , full article, gab.

  10. latwal_2: Formalization of Trellises and Tolerance Relations by Adam Grabowski, Franciszek Turowski (submitted December 27, 2024)
    39 theorems, 16 definitions, no schemes, 25 registrations, authors:Adam Grabowski. Franciszek Turowski, abstract, semantically linked, FM , full article, gab.

  11. ndiff13: Higher-Order Differentiation and Inverse Function Theorem in Real Normed Spaces by Kazuhisa Nakasho, Yasunari Shidama (submitted December 24, 2024)
    66 theorems, 3 definitions, no schemes, no registrations, authors:Kazuhisa Nakasho. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  12. newton07: Pascal's Triangle and Lucas's Theorem by Rafal Ziobro (submitted December 24, 2024)
    102 theorems, 3 definitions, no schemes, 35 registrations, authors:Rafal Ziobro, abstract, semantically linked, FM , full article, gab.

  13. vectsp13: Some Standard Examples of Vector Spaces by Christoph Schwarzweller, Agnieszka Rowinska-Schwarzweller (submitted December 24, 2024)
    41 theorems, 24 definitions, no schemes, 34 registrations, authors:Agnieszka Schwarzweller. Christoph Schwarzweller, abstract, semantically linked, FM , full article, gab.

  14. proofs_1: Fundamentals of Finitary Proofs by Taneli Huuskonen (submitted December 24, 2024)
    25 theorems, 36 definitions, 3 schemes, 38 registrations, authors:Taneli Huuskonen, abstract, semantically linked, FM , full article, gab.

  15. number16: Elementary Number Theory Problems. Part XVI by Karol Pak (submitted December 14, 2024)
    40 theorems, no definitions, no schemes, no registrations, authors:Karol Pak, abstract, semantically linked, FM , full article, gab.

  16. pdlax: Classical Isoperimetric Theorem by Kazuhisa Nakasho, Yasunari Shidama (submitted December 14, 2024)
    17 theorems, no definitions, no schemes, no registrations, authors:Kazuhisa Nakasho. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  17. glpacy00: About Path and Cycle Graphs by Sebastian Koch (submitted December 9, 2024)
    47 theorems, 10 definitions, no schemes, 98 registrations, authors:Sebastian Koch, abstract, semantically linked, FM , full article, gab.

  18. ndiff12: Differentiability Properties of Lipschitzian Bilinear Operators in Real Normed Spaces by Kazuhisa Nakasho, Yasunari Shidama (submitted December 9, 2024)
    21 theorems, no definitions, no schemes, no registrations, authors:Kazuhisa Nakasho. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  19. measur14: Universality of Measure Space by Noboru Endou, Yasunari Shidama (submitted December 9, 2024)
    55 theorems, 12 definitions, no schemes, 1 registration, authors:Noboru Endou. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  20. ascoli2: Ascoli-Arzela's Theorem (Metric Space Version) by Keiichi Miyajima, Hiroshi Yamazaki (submitted November 28, 2024)
    21 theorems, 6 definitions, no schemes, 4 registrations, authors:Keiichi Miyajima. Hiroshi Yamazaki, abstract, semantically linked, FM , full article, gab.

  21. dualsp06: Formalization of Orthogonal Complements of Normed Spaces by Hiroyuki Okazaki (submitted November 28, 2024)
    25 theorems, 6 definitions, no schemes, no registrations, authors:Hiroyuki Okazaki, abstract, semantically linked, FM , full article, gab.

  22. e_trans2: Formal Proof of Transcendence of the Number $e$. Part II by Yasushige Watase (submitted November 17, 2024)
    42 theorems, 9 definitions, no schemes, 2 registrations, authors:Yasushige Watase, abstract, semantically linked, FM , full article, gab.

  23. e_trans1: Formal Proof of Transcendence of the Number $e$. Part I by Yasushige Watase (submitted November 17, 2024)
    38 theorems, 10 definitions, no schemes, 8 registrations, authors:Yasushige Watase, abstract, semantically linked, FM , full article, gab.

  24. number15: Elementary Number Theory Problems. Part XV -- Diophantine Equations by Karol Pkak, Artur Kornilowicz (submitted November 8, 2024)
    90 theorems, 16 definitions, 1 scheme, 74 registrations, authors:Artur Kornilowicz. Karol Pkak, abstract, semantically linked, FM , full article, gab.

  25. classes5: U-Small and U-Locally Small Categories by Roland Coghetto (submitted November 8, 2024)
    111 theorems, 37 definitions, no schemes, 27 registrations, authors:Roland Coghetto, abstract, semantically linked, FM , full article, gab.

  26. surreali: Inverse Element for Surreal Number by Karol Pak (submitted October 22, 2024)
    45 theorems, 15 definitions, no schemes, 8 registrations, authors:Karol Pak, abstract, semantically linked, FM , full article, gab.

  27. number14: Elementary Number Theory Problems. Part XIV -- Diophantine Equations by Artur Kornilowicz (submitted October 22, 2024)
    112 theorems, 19 definitions, no schemes, 30 registrations, authors:Artur Kornilowicz, abstract, semantically linked, FM , full article, gab.

  28. field_15: Separable Polynomials and Separable Extensions by Christoph Schwarzweller (submitted June 18, 2024)
    94 theorems, 6 definitions, no schemes, 37 registrations, authors:Christoph Schwarzweller, abstract, semantically linked, FM , full article, gab.

  29. mesfun17: Integral of Continuous Three Variable Functions by Noboru Endou, Yasunari Shidama (submitted June 18, 2024)
    69 theorems, no definitions, no schemes, no registrations, authors:Noboru Endou. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  30. number13: Elementary Number Theory Problems. Part XIII by Artur Kornilowicz, Rafal Ziobro (submitted June 18, 2024)
    54 theorems, 5 definitions, no schemes, 13 registrations, authors:Artur Kornilowicz. Rafal Ziobro, abstract, semantically linked, FM , full article, gab.


Full list in reversed historical order (start querying) and lexical order of MML Id, titles, authors.
  1. version 5.94.1493
  2. version 5.68.1412 [differences]
  3. version 5.57.1355 [differences]
  4. version 5.45.1305 [differences]
  5. version 5.33.1254 [differences]
  6. version 5.25.1220 [differences]
[Compare two versions]
Grzegorz Bancerek: bancerek (at) mizar.org