For example, here it is in Coq (not using -- but instead replicating explicitly -- the built-in definitions of 0, 1, 2, +, or =).

  Inductive eq' {T: Type} (x: T) : T -> Prop :=
    | eq_refl': eq' x x.

  Inductive nat' :=
    | zero
    | succ (n: nat').

  Definition one := succ zero.
  
  Definition two := succ (succ zero).
  
  Fixpoint plus' (a b: nat') : nat' :=
    match a with
      | zero => b
      | succ x => succ (plus' x b)
      end.
  
  Theorem one_plus_one_equals_two : eq' (plus' one one) two.
  Proof.
    apply eq_refl'.
  Qed.

As you allude to, there's also the underlying type theory and associated logical apparatus, which in this case give meaning to "Type", "Prop", "Inductive", "Definition", "Fixpoint", and "Theorem" (the latter of which is syntactic sugar for "Definition"!), and allow the system to check that the claimed proof of the theorem is actually valid. I haven't reproduced this here because I don't know what it actually looks like or where to find it. (I've never learned or studied the substantive content of Coq's built-in type theory.)

We would also have to be satisfied that the definitions of eq', one, two, and plus' above sufficiently match up with what we mean by those concepts.