What is a number again?
Last updated: Nov. 1, 2016
The Definition of the set of natural numbers
is given by nothing more or less than
Peano’s Axioms.
Click for full text
A software tool developed by author, Dan Christensen, to teach the basic methods of mathematical proof
DC Proof 2.0 
I quote Roger Godement: ” On a calculé que,si l’on cherchait à écrire en langage formalisé un objet mathématique aussi simple (en apparence…) que le nombre 1, on trouverait un assemblage comportant plusieurs dizaines de milliers de signes (les signes fondamentaux sont en très petit nombre,, mais chacun d’eux peut naturellement étre répété un grand nombre de fois dans un même assemblage). Le mathématician qui essaierait de manipuler de pareils assemblages ressemblerait à l’alpiniste qui, pour choisir ses points d’appui sur une paroi rocheuse, examinerait celle-ci au microscope électronique”
Google translation:
“We calculated that if we wanted to write in a formalized language as simple mathematical object (apparently …) the number 1, we find an assembly comprising several tens of thousands of characters (the fundamental signs are very small many,, but each can of course be repeated many times in the same assembly). The mathematician who tries to manipulate such assemblies look like the mountaineer who, to choose its support points on a rock wall, consider this electron microscope ”
As I often say, constructing a formal proof can be a bit like building the Taj Mahal one molecule at a time. It really helps to have the right tools.