This question resolves YES to all dates by which someone can install a formatter for Lean in VSCode. This can either be through the main Lean VSCode extension, or another official extension of the Lean FRO or Lean prover community.

At a minimum, the formatter must be able to ensure theorem declarations with multi-line statements using 4 spaces for lines after the first, and the first line of the proof body being indented 2 spaces.