sorry

証明の細部を埋める前にコンパイルが通るようにしたいとき、証明で埋めるべき箇所に sorry と書くとコンパイルが通るようになります。ただし、sorry を使用しているという旨の警告が出ます。

-- Fermat の最終定理
def FermatLastTheorem :=
  ∀ x y z n : Nat, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

theorem flt : FermatLastTheorem :=
  sorry

舞台裏

Lean.Elab.admitGoal を使用することで sorry と同様のタクティクを作ることができます。

open Lean Elab Tactic

elab "my_sorry" : tactic => withMainContext do
  let goal ← getMainGoal
  admitGoal goal

theorem flt' : FermatLastTheorem := by
  my_sorry