New Feature: Lean Language Syntax Highlighting Is Now Supported!

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