CICM 2016 tutorial - exercises

  1. Define Liouville numbers
  2. Show that in the definition of Liouville numbers taken from Wikipedia the quantification of n can be replaced from "every positive integer" into "non-zero natural number".
  3. Prove auxiliary lemma that powers of two are unbounded, i.e., for any integer d, there exists a non-zero natural number such that 2 to_power (n - 1) > d.
  4. Prove that no Liouville number can be rational (follow the proof from Wikipedia).
Vocabulary file (should be in dict subdirectory)

Exercises with skeletons of proofs (should be in text directory)

Complete formalization

mizar.el should be copied to your Mizar home directory (original file can be replaced).