Formally what is a mathematical construction?

This is a bit ambiguous, as all natural language is ambiguous (especially when used in proximity to mathematical language which is not, or at least should not be, ambiguous)

Generally speaking, in mathematics you work in a context where you have a universe of objects. These could be sets, or functions, or numbers, or all of them.

When we construct something, we show that there is a way to define an object (or sometimes a collection of objects) which satisfies the properties making it "worth the name" of its construction. This formaly validates our claim as to the existence of something.

  1. When we say that we "construct a sequence", then we mean to say that we define the sequence.

  2. When we say that we "construct the real numbers", then we argue that given just the rational numbers and some background universe with "enough sets and functions", then we can define an object which has the same behavior we expect from the real numbers. We can then show that this structure is indeed unique up to isomorphism, so the method of construction (Dedekind completion, Cauchy completion, etc.) is in fact irrelevant.

The idea is that a construction usually involves some objects to start with. It could be the rationals, or a specific number used to bootstrap a sequence, or just the empty set. And from that object we define another object, in a reasonably explicit way.

For example, you cannot define a function $f\colon\Bbb R\to\Bbb R$ such that $f(x+y)=f(x)+f(y)$ and $f$ is not continuous, we know that because there are universes of mathematics where no such function exists. However, if you are given a Hamel basis for $\Bbb R$ over $\Bbb Q$, then from that basis you can construct such function (and it follows that in the aforementioned universes, no Hamel bases exist either).


What does "construction" mean formally in this context of introducing new objects?

If you were to set out to formally "construct," say, the set of real numbers, from scratch, you would have to begin with a list of axioms and rules of inference that would have to include at least one axiom that postulates the existence of some object, usually some set X with certain properties.

Your axioms and rules of inference should allow you to infer the existence of (i.e. construct) new sets given the existence of others. So, starting with set X, you would construct one set after another in this way until you have the set of real numbers.