SPARKやDesign by Contractな環境が「こいつの説明に矛盾が無いか、説明しつくしていない部分が存在しないのかを全自動で完璧にガチガチに検証してくれる環境」であるとすると、
Lean 4は「こいつの説明に矛盾が無いか見てみる」程度であって、ぜんぜん推論してくれない感じ？＞＜；