Topics - Mizar

• Definitions in Mizar
  • Example Definitions in Finite Group Theory
• Adjectives in Mizar
• Schemes
• Idiomatic Mizar from what I glean from the articles
• "Maps" or "analytical table of contents" for existing material in the MML:
  • Group Theory in Mizar
  • Ring Theory
  • Point-set Topology — a Rosetta stone
  • Linear Algebra — another Rosetta stone
  • Differential Geometry
  • Number Systems in Mizar
• Outlines and sketches of potential topics to formalize:
  • Subgroup Series
  • Matrix Groups
  • Modules and tensor products
  • Lie Theory
  • Algebraic Groups
  • Proof by Minimal Counter-Example in finite group theory
• "Element of" type
• "Function of" type

Theoretical topics:

• Mathematical Foundations of Mizar, discussing the axiomatic set theory of Mizar
• "Write Once, Compile Anywhere" philosophy of foundations: can Mizar be "foundations independent"?

Elsewhere:

• Skeletons of various statements
• Dictionary of Mathematical Notations in Mizar
• Proof Wiki pages linked to Mizar proofs
• Historic examples of formalizing math in Mizar:
  • Borsuk (1987)
  • Heyting (1987)
• Discussion of empty types occurred over the years, I last stopped at Nov 2007 where there was a huge discussion
  • Freek Wiedijk, Why do Mizar types have to be non-empty? Wed, 2 Oct 2002 11:46:30 +0200 (MET DST)
  • Wiedijk, Re: [mizar] weak types. Thu, 13 Nov 2003 09:44:10 +0100 (MET)
  • Wiedijk, Once more: empty types. Mon, 5 Nov 2007 14:13:21 +0100