話你知/Lean語言

Lean是一門以定理證明為核心的函數式編程語言，同時也是一個交互式的數學證明助手。簡單來說，它的核心作用是用代碼的形式「嚴格證明數學命題的正確性」，而非單純編寫可執行程序。因為數學裏的定理證明常依賴人工推導，容易出現疏漏。而Lean語言則像一個「數學質檢員」，你需要把證明步驟用它的語法寫成代碼，它會逐行檢查每一步推導是否符合邏輯規則，確保證明完全嚴謹、無漏洞。\大公報記者盧靜怡