心得：為何lean設計成那樣.md#

因為邏輯系統的自動證明，按照 Robinson 的 Resolution 那種算法，會產生 2^n 等級以上的推論樹， 所以不能用『自動證明』的方式。

於是由人來手寫推論過程，進行證明。

這些推論過程，可以透過數學的各種理論 (例如：群論，體論，.....) ，套用後就不需要重複撰寫。

於是整套體系就會建立起來，在 lean 的 mathlib 裏的就是這些。（包含很多定理，法則，....）