So finally, I come to this point: how a theorem could be proved using a computer? Or, equivalently, how exactly an automated proof assistant works?

This question turns out to belong to the field of constructive logic, and is answered by the famous Curry-Horward correspondence, which links the field of natural deduction and typed lambda calculus. For more details of this astonishing discovery, please refer to Propositions as Types by Philip Wadler. (You may also be interested in his talk, and this lecture note)

In short, Curry-Horward correspndance says that a Proposition in logic is just a Type in typed lambda calculus, and a Proof of that Proposition is just a term belong to that Type.

How to understand this?

Intuitively speaking, a proposition is a claim, a claim of something to be true. So we can define a data type(inductive data type as in dependent type theory) which is in equivalent to the claim(Or just define the data type recursively following the deduction definition of the claim). By doing so, if we can successfully implement an instance(or term, or element) of this data type, we are just proving the claim to be true!(i.e. the proposition is proved). On the contrary, if we can see the data type(the set) to be empty, then the proposition can not be proved.

Always, there are multiple ways to prove a proposition. Equivalently, there are multiple terms(or element) belonging to(or inside) the same data type. To prove a proposition, we just need one way of proving. Correspondingly, we just need to build one term belonging to that data type. That begins the story of automated proof assistant.

To demonstrate the idea, let me show you an example using Agda:

Example: equality

Proposition as type has a direct consequence, that is, mainly, we prove by constructing.

infix 4 _==_
data _==_ {a} {A : Set a} (x : A) : A -> Set a where
  instance refl : x == x
{-# BUILTIN EQUALITY _==_ #-}

The code above just defines a data type: ==, and has only one constructor: refl. Then, if we want to prove two terms are in equal, we just need to use these two terms to construct a term/element of == type. For example:

sym : {l : Level} -> {A : Set l} {x y : A} -> x == y -> y == x
sym {x = x} {y = .x} refl = refl

This example says, given the assumption that x==y, we want to prove y==x, that is, the equality is of reflexivity.

To prove this, we firstly build a term of assumption x==y. This is constructed by {x = x} {y = .x} refl, that is, we set x and y to be the same item, and build the equality using refl constructor.

Then we immediately has the term of second type y == x by using refl constructor! Note that we can do so because the term we put into {} is implicit, meaning that we can allow agda to do the type inference for us. And remember sym is indeed a function, which given a term of the assumption type, return a term of the correspondence type.