- Define Liouville numbers
- 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".
- 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.
- Prove that no Liouville number can be rational (follow the proof from Wikipedia).

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

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