RFC: Streamlined Entry of LaTeX Math Blocks in Markdown

Proposal

This proposal suggests improving the Lean authoring experience by supporting a convenient way to wrap selected Markdown content as a $LaTeX$ math block—e.g., by allowing users to select a block and press $ to wrap it automatically. This is an editor-level improvement aimed at reducing friction when authoring math-rich documentation in Lean.

• User Experience: Entering $LaTeX$ math in Markdown currently requires manually typing $$ before and after each math block, which can be repetitive and error-prone. A simple keyboard interaction to wrap selected content in math delimiters would improve speed and reduce mechanical burden, especially when editing complex mathematical documentation.

• Beneficiaries: Users writing Lean documentation that involves $LateX$ math expressions.

• Maintainability: Will this change streamline code maintenance or simplify its structure? N/A

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

Relevant Zulip discussion. Relevant pull request 625.

During the discussion, it was noted that while it would be ideal to allow this behavior to be user-configurable, the current capabilities of VS Code’s language-configuration.json do not expose an API for dynamic reconfiguration. Alternative mechanisms (such as a custom editor command or extension-level configuration) may be necessary to support this feature.

Impact

This proposal aims to improve the productivity of Lean users when working with Markdown and $LaTeX$ math. If you believe this feature would be valuable, please add a 👍 to the issue or share it with others who might benefit.

Review the linked Zulip discussion and pull request 625 first; the issue provides no file or test entry point. Compare the proposed VS Code language-configuration approach with the custom command or extension-configuration alternatives, and treat an agreed implementation path and documented behavior as done.