鏈

---

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

---

鏈 （英文︰Lean）者，電腦之證明助手也，一作函數式編程語言。二零一三年，美人莫拉創製於微軟。鏈其法採遞歸類型之演算，有庫名曰數學庫（英文︰mathlab），羣英獻力，欲以形式化今之數學。蓋數學證明，常艱深晦澀，而卷帙可觀，倘以人力校之，誠屬不易，亦不免於紕漏；若譯爲鏈語，則鏈程序可徑驗其正誤，迅捷可靠，是故數學家留心鏈者眾。