TY - RPRT TI - Formal Proof of the Weak Goodstein Theorem AU - Jean-Raymond Abrial PY - 2016 UR - https://arxiv.org/abs/1701.01673 ID - 1701.01673 ER -