As an aside, if you like the idea of proving theorems by programming, you can try a dependently typed language, like the Haskell-based language Agda:

For your better understanding…
* First let us define natural numbers
data Nat : Set where
zero : Nat –Zero is a natural number
suc : Nat -> Nat –Every natural number has a successor
one = suc zero –definition of 1
two = suc one –definition of 2

* Addition gets defined as follows
_+_ : Nat -> Nat -> Nat
zero + y = y
(suc x) + y = suc (x + y)

* Now let us define equality
data _==_ {A : Set}(x : A) : A -> Set where
refl : x == x –Everything is equal to itself

* Finally, let us prove a theorem
* Types are propositions
* Objects of a type are proofs of the proposition
thm : (one + one) == two –thm is a proof of 1+1=2
thm = refl –and here is the proof

Of course, this is not much different from what we can already do at runtime in Haskell. However, Agda’s type-checker allows us to check proofs statically (that is, if your proof compiles then it is correct), and it can also prove more powerful theorems, like:

* first let us prove a simple lemma
suc-subs : (x y : Nat) -> x == y -> suc x == suc y
suc-subs x .x refl = refl

* This can of course be generalized to any type
* and any type from that function

* then we can prove a less trivial theorem
plus-assoc : (x y z : Nat) -> ((x + y) + z) == (x + (y + z))
plus-assoc zero y z = refl
plus-assoc (suc x) y z = suc-subs ((x + y) + z) (x + (y + z)) (plus-assoc x y z)
* this is a proof by induction on x,
* using our lemma for the inductive step

Thanks