Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?
In order with the explicit questions:


Yes
Yes
No


To answer the question I think you're attempting to ask, we can prove many things using type checking, but not everything. What does this have to do with programs? That's what the Curry-Howard correspondence tells us. The Curry-Howard correspondence is a relationship between logic and computational models. The informal version is "proofs and programs and programs are proofs". While the specifics are far too much to detail here, the rough idea is that a function (read program) that takes an input of type $A$ and produces an output of type $B$ is a proof that $A \rightarrow B$ (and yes the funtion type arrow maps to the logical implication arrow).

Why can't we do everything? The good old halting problem. Some things we just can't check. Even worse, in practice, we're often limited to things we already know we can check, i.e. programs that are of a subclass that we know always halt.

Just to give a more complicated example, I've written a proof/program for $1+\ldots n = \frac{n\cdot(n+1)}{2}$ in Coq. Coq is a bit different to Haskell, but the idea should be fairly apparent. In this case, Coq has the advantage that it's explicitly built for theorem proving, so we can get a "proof-like" version and a "program-like" version. The proof can only complete if all the types match correctly - i.e. if we can specify a way to get from the input type to the output type, in the normal type checking sense. To avoid using division, I've rephrased the lemma.

The proof-like version:

Fixpoint sum (n : nat) : nat :=
match n with
| 0 =&gt; 0
| S n' =&gt; n + sum n'
end.

Lemma sum_closed_form (n : nat) : 2 * sum n = n * (n + 1). 
Proof.
  induction n.
  reflexivity.
  assert (Step: sum (S n) = S n + sum n).
    reflexivity.
  rewrite Step.
  rewrite mult_plus_distr_l.
  rewrite IHn.
  assert (Id : S n = n + 1).
    omega.
  rewrite Id.
  repeat rewrite mult_plus_distr_l.
  repeat rewrite mult_plus_distr_r.
  omega.
Qed.


So apart from the individual steps being black boxes, it's fairly clear that this looks a lot like a normal proof - it is in fact an induction, and all the mystery black boxes are in fact just other proofs that allow us to take some input type to another. One of the key steps in understanding how this works is to look closely at statement of the lemma: Lemma sum_closed_form (n : nat) : 2 * sum n = n * (n + 1).

Notice that it looks a bit like a function declaration, it takes a parameter of type nat, and produces an output of type 2 * sum n = n * (n + 1). That is in fact what it is, so in this form we can see the proof bit, and get an idea of the function bit - i.e. the proof is in fact a program. More explicitly, it is this program:

sum_closed_form = 
fun n : nat =&gt;
nat_ind (fun n0 : nat =&gt; 2 * sum n0 = n0 * (n0 + 1)) eq_refl
(fun (n0 : nat) (IHn : 2 * sum n0 = n0 * (n0 + 1)) =&gt;
(fun Step : sum (S n0) = S n0 + sum n0 =&gt;
eq_ind_r (fun n1 : nat =&gt; 2 * n1 = S n0 * (S n0 + 1))
(eq_ind_r (fun n1 : nat =&gt; n1 = S n0 * (S n0 + 1))
(eq_ind_r (fun n1 : nat =&gt; 2 * S n0 + n1 = S n0 * (S n0 + 1))
((fun Id : S n0 = n0 + 1 =&gt; eq_ind_r
(fun n1 : nat =&gt; 2 * n1 + n0 * (n0 + 1) = n1 * (n1 + 1))
(eq_ind_r (fun n1 : nat =&gt;
n1 + n0 * (n0 + 1) = (n0 + 1) * (n0 + 1 + 1))
(eq_ind_r (fun n1 : nat =&gt;
2 * n0 + 2 * 1 + n1 = (n0 + 1) * (n0 + 1 + 1))
(eq_ind_r (fun n1 : nat =&gt;
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n1)
(eq_ind_r (fun n1 : nat =&gt;
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n1 + (n0 + 1) * 1)
(eq_ind_r (fun n1 : nat =&gt;
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n1 + (n0 + 1) * 1 + (n0 + 1) * 1)
(eq_ind_r (fun n1 : nat =&gt;
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n0 * n0 + 1 * n0 + n1 + n1)
(Decidable.dec_not_not
(2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n0 * n0 + 1 * n0 + (n0 * 1 + 1 * 1) +
(n0 * 1 + 1 * 1))
(dec_eq_nat (2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1))
(n0 * n0 + 1 * n0 + (n0 * 1 + 1 * 1) + (n0 * 1 + 1 * 1)))
(fun H : 2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) &lt;&gt; n0 * n0 + 1 * n0 +
(n0 * 1 + 1 * 1) + (n0 * 1 + 1 * 1) =&gt;
(fun (P : Z -&gt; Prop) (H0 : P (Z.of_nat 2 * Z.of_nat (sum n0))%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_mul 2 (sum n0)))
(fun x : Z =&gt; x = Z.of_nat (n0 * (n0 + 1)) -&gt; False)
((fun (P : Z -&gt; Prop)
(H0 : P (Z.of_nat n0 * Z.of_nat (n0 + 1))%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_mul n0 (n0 + 1)))
(fun x : Z =&gt; (2 * Z.of_nat (sum n0))%Z = x -&gt; False)
((fun (P : Z -&gt; Prop) (H0 : P (Z.of_nat n0 + Z.of_nat 1)%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_add n0 1))
(fun x : Z =&gt; (2 * Z.of_nat (sum n0))%Z =
(Z.of_nat n0 * x)%Z -&gt; False)
(fun _ :  (2 * Z.of_nat (..))%Z =
(Z.of_nat n0 * (.. + 1))%Z =&gt;
(fun  (P : Z -&gt; Prop) (H0 : P (..)%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_add (..) (..)))
(fun x : Z =&gt; Z.of_nat (..) = x -&gt; False)
((fun (P : ..) (H0 : ..) =&gt; eq_ind_r P H0 (..))
(fun x : Z =&gt; .. = ..%Z -&gt; False)
(fun _ : .. =&gt; (..) (..) (..) (..)))
(inj_eq  (sum (S n0)) (S n0 + sum n0) Step))))
(inj_eq (2 * sum n0) 
(n0 * (n0 + 1)) IHn)))
(mult_plus_distr_r n0 1 1))
(mult_plus_distr_r n0 1 n0))
(mult_plus_distr_l (n0 + 1) n0 1))
(mult_plus_distr_l (n0 + 1) (n0 + 1) 1))
(mult_plus_distr_l n0 n0 1)) 
(mult_plus_distr_l 2 n0 1)) Id)
(Decidable.dec_not_not (S n0 = n0 + 1)
(dec_eq_nat (S n0) (n0 + 1))
(fun H : S n0 &lt;&gt; n0 + 1 =&gt;
(fun (P : Z -&gt; Prop)
(H0 : P (Z.of_nat 2 * Z.of_nat (sum n0))%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_mul 2 (sum n0)))
(fun x : Z =&gt; x = Z.of_nat (n0 * (n0 + 1)) -&gt; False)
((fun (P : Z -&gt; Prop)
(H0 : P (Z.of_nat n0 * Z.of_nat (n0 + 1))%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_mul n0 (n0 + 1)))
(fun x : Z =&gt; (2 * Z.of_nat (sum n0))%Z = x -&gt; False)
((fun (P : Z -&gt; Prop)
(H0 : P (Z.of_nat n0 + Z.of_nat 1)%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_add n0 1))
(fun x : Z =&gt; (2 * Z.of_nat (sum n0))%Z = (Z.of_nat n0 * x)%Z -&gt; False)
(fun _ : (2 * Z.of_nat (sum n0))%Z =
(Z.of_nat n0 * (Z.of_nat n0 + 1))%Z =&gt;
(fun (P : Z -&gt; Prop) (H0 : P (Z.of_nat (S n0) + Z.of_nat (sum n0))%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_add (S n0) (sum n0)))
(fun x : Z =&gt; Z.of_nat (sum (S n0)) = x -&gt; False)
((fun (P : Z -&gt; Prop) (H0 : P (Z.succ (Z.of_nat n0))) =&gt;
eq_ind_r P H0 (Nat2Z.inj_succ n0))
(fun x : Z =&gt; Z.of_nat (sum (S n0)) = (x + Z.of_nat (sum n0))%Z -&gt; False)
(fun _ : Z.of_nat (sum (S n0)) =
(Z.succ (Z.of_nat n0) + Z.of_nat (sum n0))%Z =&gt;
(fun (P : Z -&gt; Prop) (H0 : P (Z.succ (Z.of_nat n0))) =&gt;
eq_ind_r P H0 (Nat2Z.inj_succ n0))
(fun x : Z =&gt; Zne x (Z.of_nat (n0 + 1)) -&gt; False)
((fun (P : Z -&gt; Prop) (H0 : P (Z.of_nat n0 + Z.of_nat 1)%Z) =&gt;
eq_ind_r P H0 (Nat2Z.inj_add n0 1))
(fun x : Z =&gt; Zne (Z.succ (Z.of_nat n0)) x -&gt; False)
(fun H0 : Zne (Z.succ (Z.of_nat n0))
(Z.of_nat n0 + 1) =&gt; ex_ind (fun (Zvar29 : Z)
(Omega75 : Z.of_nat n0 = Zvar29 /\ (0 &lt;= Zvar29 * 1 + 0)%Z) =&gt;
and_ind (fun (Omega66 : Z.of_nat n0 = Zvar29)
(_ : (0 &lt;= Zvar29 * 1 + 0)%Z) =&gt;
ex_ind (fun (Zvar30 : Z) (Omega74 : .. /\ ..%Z) =&gt;
and_ind (.. =&gt; ..) Omega74) (intro_Z (sum (..)))) Omega75)
(intro_Z n0))) (inj_neq (S n0) (n0 + 1) H)))
(inj_eq (sum (S n0)) (S n0 + sum n0) Step))))
(inj_eq (2 * sum n0) (n0 * (n0 + 1)) IHn)))) IHn)
(mult_plus_distr_l 2 (S n0) (sum n0))) Step) eq_refl) n
: forall n : nat, 2 * sum n = n * (n + 1)


To give a shorter example, the associativity of addition can be proved like so:

Lemma add_assoc (n m p : nat) : n + (m + p) = (n + m) + p.
Proof.
  induction n.
  reflexivity.
  simpl. rewrite IHn.
  reflexivity.
Qed.


The associated function is:

add_assoc = 
fun n m p : nat =&gt;
nat_ind (fun n0 : nat =&gt; n0 + (m + p) = n0 + m + p) eq_refl
  (fun (n0 : nat) (IHn : n0 + (m + p) = n0 + m + p) =&gt;
   eq_ind_r (fun n1 : nat =&gt; S n1 = S (n0 + m + p)) eq_refl IHn) n
     : forall n m p : nat, n + (m + p) = n + m + p