We insert an HTML comment to avoid a `$` right before a digit, which pandoc will not recognize as a math delimiter.