Hi!
The Lean track is being tested right now and should launch in a few days.
The next step after that is adding static and dynamic syntax highlighting.
Static highlighting
Highlight.js has support to Lean, via a third-party plugin. This plugin is published on NPM.
In this case, the instructions mention to start a topic on the forum requesting to add support for the plugin to the website.
Dynamic highlighting
There is no out of the box codemirror support for Lean and I also couldn’t find any codemirror plugin for the language. Of the options available, I believe Haskell is the one with the syntax closest to Lean’s.
The instructions mention we should also open a topic on the forum requesting this.
Conclusion
In short, can someone with the powers to do so add support for this highligh.js plugin and enable codemirror support for Lean using Haskell syntax?
Thank you very much!