This is probably a naive and vague question. And perhaps I should have search first whether something like this was asked on the main. And perhaps this has intersection with the topic of logic chatroom, too.

Often when reading that something is not provable in ZF (as opposed to ZFC), I read something like this: "This means you cannot give an explicit construction of a non-measurable set." "You cannot write down an explicit well-ordering of reals.

Quotes from this site:

"It is impossible to give an explicit example of a non-Borel-measurable subset of $\mathbb{R}$." math.stackexchange.com/questions/226559/…

"In other words, it is impossible to write down a well-ordering of $\mathbb{R}$ in ZF." math.stackexchange.com/questions/6501/…

Would it be possible, that there is some explicit construction/explicit formula for some object (such as well-ordering or non-measurable set or something else choice related) but still the proof needs AC?

However, I do not know a good formalization of "explicit definition/construction/formula".

So basically I am asking: Does it make sense to make a distinction between "provable without AC" and "definable without AC"? Can something along these lines be reasonably formalized?