Mizar Proof Structure

• Limited fast checker for verifying simple inferences
  (Simple Justifications)
• Trying to capture the "obviousness" concept:
  inferences accepted by the checker should be neither too strong, nor too simple for humans to understand
• Inferences too complicated for the checker have to be decomposed into sufficiently simple inferences using structural rules (Jaskowski-style natural deduction) (Mizar Proof block)
• A part of the Mizar verifier (Reasoner) checks the correctness of the structural rules
• Additional lemmas and constants can be introduced inside Mizar proofs
• The reasoning steps inside Mizar proofs can be divided into those that modify the current "thesis", and other (Auxiliary) steps that do not (e.g., introduce a useful lemma)