The proof of commutativity for addition of natural numbers has been used as a simple pedagogical example in some places, including the Wikipedia page for Coq. It is a bit longer than just "Hello World" but it is an example that is about as simple as one can imagine for a proof, while still remaining non-trivial. This is what the code would look like for Coq:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n

The proof of commutativity for addition of natural numbers has been used as a simple pedagogical example in some places, including the Wikipedia page for Coq. It is a bit longer than just "Hello World" but it is an example that is about as simple as one can imagine for a proof, while still remaining non-trivial. This is what the proof term (quoted from the Wikipedia page) would look like for Coq:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n

However, Coq users rarely write such proof terms directly. Rather, they prove theorems with tactics. Here is a tactic-based proof of the same theorem (leading to a slightly different proof term):

Lemma plus_comm : forall n m, n + m = m + n.
  intros; induction n.
  - simpl.
    symmetry.
    apply Nat.add_0_r.
  - simpl.
    rewrite Nat.add_succ_r.
    f_equal.
    apply IHn.
Qed.

The proof of commutativity for addition of natural numbers has been used as a simple pedagogical example in some places, including the Wikipedia page for Coq. It is a bit longer than just "Hello World" but it is an example that is about as simple as one can imagine for a proof, while still remaining non-trivial. This is what the code would look like for Coq:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n
 

The proof of commutativity for addition of natural numbers has been used as a simple pedagogical example in some places, including the Wikipedia page for Coq. It is a bit longer than just "Hello World" but it is an example that is about as simple as one can imagine for a proof, while still remaining non-trivial. This is what the code would look like for Coq:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n