# Formal Proof of the Weak Goodstein Theorem

## TL;DR

This paper presents a formal proof of the Weak Goodstein Theorem, illustrating how to teach complex mathematical proofs through systematic examples and refinement, aimed at enhancing student understanding.

## Contribution

It provides a formal proof of the Weak Goodstein Theorem and demonstrates an effective approach to teaching complex proofs using examples from professional mathematics.

## Key findings

- Formal proof of the Weak Goodstein Theorem
- Educational method for teaching complex proofs
- Application of proof refinement techniques

## Abstract

For many years, I have been interested in introducing students to the development of complex systems by means of modelling and refinement. To this end, I did not find anything better than presenting many examples of system developments. However, I figured out that my examples were not explicit enough on how (mechanical) proofs are performed. So, besides courses presenting these examples and also some courses in various forms of proofs (propositional calculus, first order predicate calculus, set theory), I decided to study the work of professional mathematicians, thinking that it could be good examples for students. Among the works I already studied and reconstructed are the theorem of Zermelo, the theorem of Cantor-Bernstein, the planar graph theorem of Kuratowski, the topological proof of the infinity of primes of Furstenberg, the intermediate value theorem of Bolzano, the Archimedean property of the set of Real numbers, and others. More recently, I found that the Goodstein theorem was also very interesting. The purpose of this short note is to give some information about this theorem and the way I introduce a weak form of it to students.