鏈

---

• 是題本作Lean。顧夫文言，漢字維基。非茲入題，雅正不濟。故告示之，尚祈見諒。

---

鏈（英文︰Lean）者，助證之軟體也，亦函數之語言，通行於電算機。西元二零一三年，美人莫拉創製於微軟社。其法宗演算，兼採遞歸之類型。有庫曰數學庫（英文︰mathlib），集羣英之力，旨在化今之數學為形式。蓋數學證明，每多艱深，卷帙浩繁，以人力校之，誠屬不易，且難免紕漏。若譯為鏈文，則程序徑驗其誤，迅捷可信。是以算學家多留意焉。