说真的，Hexo 这么烂下去我真要换 Hugo 了——为什么它甚至不支持给 hljs 添加语言插件？
好吧，这篇博客讲述如何让你的 Hexo 博客支持高亮 Lean，并且是后端渲染。
Step 1. 安装 highlightjs-lean ¶
问题的起因就是 hljs 并不默认支持 lean，因此必须手动安装之。在你的 hexo 博客根目录进行：
npm install highlightjs-lean
# 或者 yarn add highlightjs-lean
Step 2. 将 Lean 语言支持添加到 hljs ¶
你需要创建一个简单的 hexo 插件做这件事情。在你的 hexo 博客根目录新建 scripts 文件夹，随意新建一个 javascript 文件，名字自取，例如 add-lean.js
在该 js 文件中写入以下内容：
const hljs = require("highlight.js");
const leanHljs = require("highlightjs-lean");
hljs.registerLanguage("lean", leanHljs);
这样就注册了 lean 的语言支持
Step 3. 把 hexo-utils 的语言定义文件里添加上 Lean ¶
如果你做了上述操作，恭喜你，至少 autodetect 能尝试识别 Lean 了。但是 hljs 的 autodetect 众所周知的不准确，于是你尝试在代码块中指定语言为 lean，嘿，hexo 反而自动给你转成 plaintext 了~
在这三行中揭示了原因。 hexo-utils 使用了一个 hard-coded 的 highlight_alias.json 文件，任何不在这个 json 文件中的语言都会直接被视作 plaintext， 我不懂它为什么要这样干，hljs 明明提供了 api 让你获得 available 的语言，但它就是这么干了。
const alias = require('../highlight_alias.json');
function highlight(str: string, options: Options) {
//...
if (!lang || !alias.aliases[lang]) {
lang = 'plaintext';
}
由于这个文件是硬编码的，你甚至不能更改它。所以插件在这里有些苍白无力。你不得不写一个 不是插件的脚本（比如 pre-deploy.js），在每次 deploy 前把该文件修改一下：
const fs = require("fs");
const alias = JSON.parse(
fs.readFileSync("node_modules/hexo-util/highlight_alias.json").toString()
);
alias.aliases["lean"] = "lean";
alias.languages.push("lean");
fs.writeFileSync(
"node_modules/hexo-util/highlight_alias.json",
JSON.stringify(alias)
);
然后在你每次 deploy 前，需要执行一下
node pre-deploy.js
把该文件修改后，hexo 终于支持了 lean 语言的高亮。
或者…… ¶
不跟你 hexo 的 markdown 渲染器玩辣！
安装 markdown-it-highlightjs，作为 markdown-it 的插件，关掉 hexo 的 highlight 处理。现在 Step3 的所有内容直接可以不看，Lean 4 高亮已经好了。
成果展示 ¶
import MIL.Common
open Nat
-- These are pieces of data.
#check 2 + 2
def f (x : ℕ) :=
x + 3
#check f
-- These are propositions, of type `Prop`.
#check 2 + 2 = 4
def FermatLastTheorem :=
∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n
#check FermatLastTheorem
-- These are proofs of propositions.
theorem easy : 2 + 2 = 4 :=
rfl
#check easy
theorem hard : FermatLastTheorem :=
sorry
#check hard
-- Here are some proofs.
example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
show ∃ l, m * n = l + l from ⟨_, hmn⟩
example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩
example : ∀ m n : Nat, Even n → Even (m * n) := by
-- Say m and n are natural numbers, and assume n=2*k.
rintro m n ⟨k, hk⟩
-- We need to prove m*n is twice a natural number. Let's show it's twice m*k.
use m * k
-- Substitute for n,
rw [hk]
-- and now it's obvious.
ring
example : ∀ m n : Nat, Even n → Even (m * n) := by
rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring
example : ∀ m n : Nat, Even n → Even (m * n) := by
intros; simp [*, parity_simps]