[kmill]

The system used in Lean 4 is explained in https://arxiv.org/abs/2001.10490v7 (Ullrich and Moura, "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages").

There's still a set-of-scopes system, but it seems to be pretty different from https://users.cs.utah.edu/plt/scope-sets/ (And to clarify what I wrote previously, each identifier has a list of macro scopes.)

The set-of-scopes in Lean 4 is for correct expansion of macro-creating-macros. The scopes are associated to macro expansions rather than binding forms. Lean's syntax quotations add the current macro scope to every identifier that appears in quotations in the expansion. That way, if there are multiple expansions of the same macro for example, it's not possible for identifiers in the expansion to collide. There's an example in section 3.2 of a macro macro that defines some top-level definitions.

(Section 8 of the paper, related work, suggests that set-of-scopes in Lean and Racket are closer than I'm understanding; I think what's going on is that Lean has a separate withFreshMacroScope primitive that macros can invoke, and syntax quotations participate in macro scopes, whereas Racket seems to give this responsibility to binding forms, and they're responsible for adding macro scopes to their binders and bodies. I'm a bit unclear on this.)