There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc.

There are also multiple possible ways to check definitional equality (an essential part of typechecking for a dependently typed language). For normalization, there is traditional step-by-step $\beta$-reductions, using different strategies such as call-by-name, call-by-value, or call-by-need, and similarly using or not using explicit substitutions, and other variations. There is also normalization-by-evaluation, which also has variations such as whether closures are defunctionalized. And an equality-checking algorithm can use normalization in different ways, e.g. it could just normalize both terms all the way (perhaps including $\eta$-expansion or not) and compare the normal forms, or it could traverse them step-by-step mimicking a normalization algorithm and comparing as it goes. It could also try a "short-circuit" comparison of not-fully-normalized terms in hopes of detecting some equalities faster before falling back on full normalization, and I'm sure there are many other variations.

There are lots of interesting theoretical arguments to be made about which combinations of these choices are better (and for which purposes); for instance, one "sweet spot" theoretically seems to be normalization-by-evaluation with De Bruijn indices for unevaluated "terms" and De Bruijn levels for evaluated "values".

But what I want to know right now is what implementations of real-world dependently typed proof assistants actually do, today, to represent bound variables and check equality.

Specifically, I want to know what combinations of choices have actually proven to scale effectively and efficiently in practice. Thus, by "real-world" I mean a proof assistant that's used by significant numbers of people for large-scale formalization projects. I'm particularly interested in Coq, Agda, and Lean, since I have the most experience with them, but I would also be interested in answers addressing other proof assistants that fit those criteria.