看起來 Lean 今天很受歡迎，所以這裡有一篇小文章，介紹它是如何運作的以及如何在 Julia 中實現一個迷你版本。

你其實不需要了解 Julia，因為這非常簡單！(而且你 _絕對_ 不需要了解 Lean)

無論如何，這是帖子

如果你更喜歡直播的話：

@outputlayer rosé pine dawn (不使用斜體)，字體是來自無可比擬的 @usgraphics 的 berkeley mono

@frang_u99393 哦，是的，依賴類型在這裡完全顯現出來，那麼 Lean 將會是類型系統的一個簡單副作用，並且還有一些額外的優點，因為你實際上可以在 Julia 中編寫軟體。

@frang_u99393 "Lean" 作為 "類似 Lean 的互動定理證明系統" 的替代詞