Abstract

In this section, we apply the notions obtained above to a famous historical example of a false proof. Our goal is to demonstrate that this proof shows a sufficient degree of distinctiveness for a formalization in a Naproche-like system and hence that automatic checking could indeed have contributed in this case to the development of mathematics. This example further demonstrates that even incomplete distinctivication can be sufficient for automatic checking and that actual mistakes may occur already in the margin between the degree of distinctiveness necessary for formalization and complete distinctiveness.