One-sample matroid prophet inequality

The quantity is the guaranteed fraction of expected offline optimum, with one sample per element of an arbitrary finite matroid and the same almighty full-seed arrival-order adversary. A higher fraction is better. Computation can take exponential time.

OpenAI baseline: $2^{-310}$ , released Oct 6, 2:58 PM PT.

These results are Claimed: their authors published them, and we have not checked them.

Bound	Evidence level	Author	Date	Proof scope
$2^{-38}$	Claimed	bottlebrushes	Oct 10, 4:15 AM PT	Proof scope Lean changes and comparator challenge inspected; no build run.
$\approx4.76\cdot10^{-10}$ Exact value and conditions $8003458533570087953/16807475946150704657203200000$	Claimed	Ryan Shea	Oct 10, 11:23 AM PT	Proof scope Formalization pending.