What is an explicit bijection in combinatorics? A standard way of demonstrating that two collections of combinatorial objects have the same cardinality is to exhibit a bijection between them. Browsing through some examples (here, there, yonder) quickly reveals that combinatorialists call such bijections explicit, presumably to differentiate them from other less palpable kinds of bijections. Wikipedia speaks of the method of bijective proof.
It seems that we have here a typical example of an informal mathematical notion that is quite familiar to most mathematicians, however it is difficult to pin down a proper and satisfying mathematical definition. I asked the local combinatorialists and did not really get a good answer.
Question: What is a proper mathematical definition of an explicit bijection?
Often we ask for an explicit bijection between two families of combinatorial objects, i.e., bijections $b_n : A_n \to B_n$, one for each $n \in \mathbb{N}$. Here $(A_n)_n$ and $(B_n)_n$ are two families of combinatorial objects, parametrized by $n$. The parameter need not be a single number.
Here are some unsatisfactory answers:


*

*"A bijection is explicit if it is computable." This definition is too wide, because it allows silly algorithms that order combinatorial objects according to the layout of the sequences of bits that represent them, and use the order to establish a bijection. Bit representations typically have nothing to do with the combinatorial content of the objects under consideration.

*"A bijection is explicit if it can be written down as an expression." This takes us back several centuries in terms of level of mathematical abstraction, and also varies a lot depending on what expressions are allowed. We really should be looking for a combinatorially meaningful notion, not a syntactic surrogate.

*"A bijection is explicit if we can give a constructive proof of its existence." Well, a constructive proof certainly guarantees that a computable bijection exists, and can moreover be extracted from the proof, but this still feels too permissive. For example, we can always compose an explicit bijection so obtained with a computable automorphism of one of the sets, and still have a constructive proof. But such an automorphism could completely obfuscate the combinatorial structure of the set.

*"Well-order $V_\omega$ (as all combinatorial objects easily live in it) and take the first bijection under the well ordering." Only a set theorist would have such thoughts. Again, we should strive for a definition which will be accepted as natural by combinatorialists.
Let me also say that I would prefer to not generalize the question to "what is an explicit thing?" At least in combinatorics "explicit bijections" are a well-established and useful notion, whereas mathematicians in general do not posses a universally agreed upon notion of "explicit thing".
Supplemental: After having a look at Igor Pak's paper, I am somewhat convinced that computational complexity plays a certain role, but it cannot be the only answer (as Pak himself notes). For example, an explicit bijection may require factoring of numbers, which I feel most people would find unproblematic even though the computational complexity of factoring is not resolved.
 A: I would say that a bijection $\pi: A\to B$ is explicit, if for every $a\in A$ the image $\pi(a)$ can be computed without reference to $B$ itself.  More precisely, suppose that $A$ and $B$ are not known, but only an element $a\in A$, then it should still be possible to construct $\pi(a)$.
In particular, sorting $B$, or iterating over $B$ to find a particular object, is not possible with this definition.
On the other hand, this allows algorithms whose well-definedness or injectivity is not obvious from the algorithm.  I think that this is in fact desirable.  
Let me contrast this definition with other concepts, which I believe
should be orthogonal to being explicit.


*

*computational complexity: a bijection may be computable in
polynomial time and memory, but still be not explicit.
For example, Dyck paths of semilength $n$ with exactly one valley are
in bijection with subsets of size $2$ in $\{1,\dots,n\}$.  A
non-explicit bijection which is computable in polynomial time is to
fix an order on the Dyck paths, and an order on the subsets and match
elements with the same index.

*simplicity: a bijection may be very complicated, but still be
explicit.
A (biased) example is Jagenteufel's bijection between Riordan paths
and standard Young tableaux with three rows, whose row lengths are
either all odd or all even, see Algorithm 3 in
https://arxiv.org/abs/1801.03780, or Algorithm 3 in
https://arxiv.org/abs/1902.03843 for a generalisation to fans of
Riordan paths.
Although this bijection is really complicated, it allows to deduce a
refinement of the equinumeration result, that is otherwise
unavailable.

*apparently bijective:
The sweep maps on lattice paths were defined by Armstrong, Loehr and
Warrington in https://arxiv.org/abs/1406.1196.  It took quite a while
to show that they are bijective, see Thomas and Williams
https://arxiv.org/abs/1512.01483.  I think that the maps were
bijective already in June 2014, and did not become bijective in
December 2015, but philosophy might disagree.
I am sure there are also examples where the only known proof of bijectivity uses enumeration, but the map itself yields other properties.

*apparently well defined:
Consider Prüfer's bijection between $(n-2)$-tuples of integers in
$\{1,\dots,n\}$ and labelled trees on $n$ vertices.  Although not
hard to see, it is not a priori clear that given a tuple one actually
obtains a tree: from the definition of the algorithm itself one might
think that the result could be forest.
A: I would like to adopt a slightly contrarian viewpoint:

There is no formal mathematical definition of "explicit bijection."

Of course, I can't formally prove this assertion, but I would say that the reason you're having trouble finding a satisfactory formal definition is precisely because there isn't one.
A similar issue comes up in the Razborov–Rudich theory of natural proofs.  Quoting from their paper:

Note that the definition of a natural proof, unlike that of a natural combinatorial property, is not precise.  This is because while the notion of a property being explicitly defined in a journal paper is perfectly clear to the working mathematician, it is a bit slippery to formalize.  This lack of precision will not affect the precision of our general statements about natural proofs because they will appear only in the form "there exists (no) natural proof…", and should be understood as equivalent to "there exists (no) natural combinatorial property $C_n$…"

Taking a cue from the above, I think that what may be more productive than trying to pin down an exact definition of an explicit bijection is finding sufficient conditions for being an explicit bijection.  I say this because I have a secret agenda: performing automated searches for explicit bijections.
For this purpose, I think it would be useful to compile a list of "atomic" components of an explicit bijection and say that if one combines no more than $x$ such components in certain specified ways, then the resulting bijection (or map, if we don't know in advance that it is bijective) is explicit.
By the way, here's an analogous issue from recreational mathematics.  What does it mean to say that a Sudoku puzzle (let's assume that it has a unique solution) can be "solved without guessing"?  I don't think that there is a canonical answer to this question, because what looks like guessing to you or me might just be a "standard trick" to a sufficiently powerful brain.  On the other hand, it is possible to compile a specific long list of known tricks, and then you can automate the generation of "Sudokus solvable without guessing."
A: This is not at all intended as a complete answer to the question, but one criterion that feels important is that for a bijection $f$ to count as explicit, one shouldn't need to know in advance that there exists a bijection in order to prove that $f$ is a well-defined bijection. So for example if you order the elements of two sets $A$ and $B$ in some way that has nothing to do with why $|A|=|B|$, then you need to know that $|A|=|B|$ in order to conclude that the bijection that maps the $k$th element of $A$ to the $k$th element of $B$ is indeed a well-defined bijection.
I think this criterion rules out 1 and 4 (or would do if one could make it more formal, which might itself not be wholly easy). 
A: One criterion not mentioned yet is naturality in the categorical sense, which can also be phrased as equivariance with respect to permutation actions.  This approach has been extensively developed by André Joyal and others, under the name of combinatorial species.
In almost all natural examples (I’m tempted to remove the “almost”), the sets $A_n$ and $B_n$ aren’t just $\mathbb{N}$-indexed families of sets; they also come with natural permutation actions, with $\Sigma_n$ acting on $A_n$ and $B_n$.  Equivalently, $A_\bullet$ and $B_\bullet$ can be seen as functors on the category $\mathrm{FinSet}_{\cong}$ of finite sets and isomorphisms; this representation is often clearest to work with.  E.g. if $A_n$ is “finite trees with $n$ leaves”, one can generalise it to a functor on $\mathrm{FinSet}_{\cong}$ by taking $A_X$ to be “finite trees with leaves labelled by $X$”; an isomorphism $\varphi : X \to Y$ gives an action $A_X \to A_Y$ by relabelling leaves.
One can then require the functions $f_n$ to be natural, in the categorical sense, with respect to this functoriality.  That is, for an isomorphism $\varphi : X \to Y$ of finite sets, and $a \in A_X$, one should have $f_Y(\varphi \cdot x) = \varphi \cdot (f_X a)$.  In terms of permutation actions, this is equivariance: $f_n(\sigma \cdot x) = \sigma \cdot f_n(x)$.
The effect of this, roughly, is to rule out constructions that involve arbitrary or non-uniform choices at any stage.  I think all examples that would traditionally be considered “natural” or “canonical” by combinatorialists are natural in this or some closely related sense — I’d be very interested to see a counterexample to that.  On the other hand, one can produce contrived examples that are natural in this sense without being “natural”: e.g. take some example with two different natural bijections $f$, $g$, and define a new one by using $f$ for even $n$, and $g$ for odd $n$.
Comparing to the other criteria suggested: this one is pretty much orthogonal to computational complexity.  It’s a bit linked to logical constructivity: there are metatheorems saying that anything definable in certain constructive logics must be natural in this sense.
A: My suggestion has quite some overlap with other comments and also @gowers answer:
Let $A$, $B$ be two sets. An explicit bijection between $A$ and $B$ is a deterministic algorithm taking elements of $A$ as input and for which outputs are elements of $B$, such that an analysis of the algorithm yield its bijectivity.
Several notes:


*

*In most cases I have been looking at, the sets $A$ and $B$ were finite.

*A typical way of satisfying this criterion is to provide two deterministic algorithms $A \to B$ and $B \to A$ and showing that they are inverses of each other. Or showing that both are injective. I would also call this "explicit" though one might need to slightly reword to include this situation.

*I did not include anything about complexity of the algorithm because I do not think its actual computation time is relevant for it being "explicit".

*I have often seen the following relaxation, namely that one knows already that $|A| = |B|$, and only deduces injectivity or surjectivity from the algorithm. The problem with this relaxation is that it would allow just listing the elements of both sets...
A: Here's an example (credit: Paul Russell) of the sort of bijection you want to rule out.
Question: Find an explicit bijection $f$ between the size-$k$ and size-$(k + 1)$ subsets of $\{1, 2, \dots, 2k+1\}$, such that $x \subset f(x)$ for all $x$.
Answer: Consider the bipartite graph with a vertex class $X$ for the size-$k$ subsets and a vertex class $Y$ for the size-$(k + 1)$ subsets; let edges $x, y$ denote $x \subset y$. The graph is regular, so a matching exists by Hall. Take the lexicographically first such matching (represented as a binary adjacency matrix).
If you try to rule this out by stipulating 'polynomial time' in your definition of explicit, then Russell's construction can be modified by replacing the last sentence with:
"Apply the Hopcroft-Karp algorithm to the initially empty matching"
Another attempt to rule out Russell's construction is to disallow someone from mentioning 'the set of all matchings', such as by type-theoretically restricting the answer to only mention sets of integers. But this approach doesn't work either, because finite sets can be encoded as integers.
Gowers' answer would rule this out if it could be made precise: by the time we invoke Hall, we know a matching exists. But if we didn't know about Hall's marriage theorem and avoided proving it until after applying the Hopcroft-Karp algorithm, we could 'cheat' the Gowers test. Also, a proof could be obfuscated, IOCCC-style, to hide the part that proves the existence of at least one matching.
What would rule out the Russell construction, whilst allowing the genuine explicit construction, is to stipulate that the bijection is computable with polynomial memory as a function of the description length of the individual objects being bijected: the full bipartite graph is exponential in $k$, whereas the objects (sets of integers) are expressible in $O(k \log k)$ symbols.
I'm going to suggest this definition unless anyone can provide a non-contrived example of an explicit combinatorial bijection that fails my test.
A: This should perhaps be a comment on the answer by Peter LeFanu Lumsdaine, but it's too long and might be relevant in connection with other answers as well. Long ago, Bruce Sagan and I wrote a paper,
Bijective proofs of two broken circuit theorems. 
J. Graph Theory 10 (1986), no. 1, 15–21,
in which we explicitly claimed, already in the title, to give bijective proofs. As far as I know, no one has yet objected to this claim, so I'll assume, in this answer, that the proofs given there are considered bijective. (Non-bijective proofs of the same results were known much earlier.) 
Each of our results exhibits a bijection between two sets, say $A_G$ and $B_G$, associated to a finite graph $G$. As already hinted in the title, the definitions of these sets involve the notion of "broken circuit".  That notion, in turn, depends on a linear ordering of the set of edges of $G$. So the $G$ subscript in $A_G$ and $B_G$ should be understood as referring not just to the graph $G$ but to the graph together with such an ordering. 
Unfortunately, a finite graph-with-edge-ordering has no nontrivial automorphisms except in some trivial cases.  In fact (again excepting trivial situations), a linear ordering of the edges is enough information to uniquely determine, in a purely combinatorial way, linear orderings of the finite sets $A_G$ and $B_G$. So we could, with the same information (and the same naturality) as in our construction, have defined the bijection between $A_G$ and $B_G$ that preserves the linear orderings. Yet no combinatorialist would call that a bijective proof.
