Let $τ(N)$ be the number of graceful labelings of trees with $N$ edges, that is, the number of spanning trees of the complete graph on $\{0,1,\dots,N\}$ whose edges have distinct lengths. The answer to exercise 7.2.2.3-106 of The Art of Computer Programming states that, if an empirical observation of Anick is true, then $τ(n)=\exp(n\ln n-n\ln(e/b)+O(\log n))$ with $b\approx0.636$, and that rigorous proofs are unknown. We prove that $|\logτ(N)-(N\log N-N\log(e/b))|\le152(1+\log(N+1))^4$ for every $N\ge3$, with $b=2/π$. A rainbow map of order $N$ sends each vertex $k\in\{1,\dots,N-1\}$ to a vertex $f(k)\in\{0,\dots,N\}$ so that the lengths $|f(k)-k|$ are $1,\dots,N-1$ in some order. Acyclic rainbow maps are exactly the graceful labelings, and all rainbow maps are counted by the Whitty numbers $W(N)$ (OEIS A134983). We show that $τ(N)\le W(N)\leτ(N)e^{151(1+\log(N+1))^4}$ by a combinatorial argument: for fixed directions, rainbow maps are rook placements on a Ferrers board; a swap injection shows that a uniformly random rainbow map has $O(\log^2N)$ cycles on average; and an inequality on the periods of a word shows that the $c$ cycles of a rainbow map can be removed by changing $O(c\log N)$ edges. We also show that $W(N)$ is the total weight of a family of weighted Motzkin paths. This yields exact enumerations, an alternating sum for $W(N)$, and a representation of $W(N)$ as a moment of a continuous dual Hahn weight, from which $|\log W(N)-(N\log(2N/π)-N)|\le5(1+\log(N+1))$. The main theorem has been formalized in Lean 4; its combinatorial half uses no axioms beyond those of Lean.