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 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 refl, that is, we need to find a term that has type x==y, but according to the definition of the family of _==_ type, we only have one constructors refl which represents x==x type. Agda finds that the only way to do so is to have a constraint on what x and y could be: they should be identical!.

And similarly, we also have the term of second type y == x by using refl constructor too! 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.

So the prove of {l : Level} -> {A : Set l} {x y : A} -> x == y -> y == x is constructed in such a way, that, since the only member of equality is refl, the equality should obey reflexivity. Look how Agda see this from a constructive perspective: it search for the possibility to build an algebra stucture, and through building, it proves the property of that algebra structure. This is a type theory perspective, not the same as set theory perspective, but they are always reaching the same point.