#lean4

Highlight proven (processed) regions of Lean 4 files in green, similar to VSRocq. Supports stepping through proof blocks with Alt+Up/Down.

LeanWeaver

fiersity

Rule-based Lean 4 error explainer — hover errors to get clear explanations. 悬停报错即懂：英语优先，可切中文。