Syntax highlighting for the Lean proof assistant is now supported across our platform!
This update comes directly in response to users’ feedback. As Lean continues to gain popularity among mathematicians, researchers, and students for writing precise, computer-verifiable proofs, we want our platform to keep pace.
✍️ How to Use It
If you write your post in markdown, you can highlight Lean code by
wrapping the code block with triple backticks and use lean
as the language identifier:
```lean
-- Proof of commutativity of addition in Lean
theorem add_comm (a b : ℕ) : a + b = b + a := by
sorry
```
It will be rendered like this:
-- Proof of commutativity of addition in Lean
theorem add_comm (a b : ℕ) : a + b = b + a := by
sorry
If you write your post in latex, you can highlight lean code like the following:
\begin{minted}{lean}
-- Proof of commutativity of addition in Lean
theorem add_comm (a b : ℕ) : a + b = b + a := by
sorry
\end{minted}
You will get the same rendering result as above.
🚧 Beta Notice
Lean syntax highlighting is currently in beta.
If you notice anything that’s not working correctly—or if you have
suggestions for improvement—we’d love your feedback:
👉 Submit feedback
here