JLimperg/aesop
White-box automation for Lean 4
概要
Lean 4の証明を一部自動化する便利なタクティクaesopを追加する. Automated Extensible Search for Obvious Proofs
simpなどを属性として持つ証明などをひたすら当ててゴールに向かって進み,得られたら証明可能とする
Lean 4のtrivialに近いが,こちらはかなり積極的に証明を探索してくれる 逆に言えばtrivialは大体のケースで「自明であってよ(泣)」という事実にすら役に立たないことが多い