Project-declaredLean 4.8.0
Alice pr le
alice_pr_le
Plain-language statement
Honest Alice has error ≥ e with probability ≤ q
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Source-pinned research
Research proof index
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 52 research declarations. Search 10,000 more complete Mathlib declarations.
52 results
Clear filtersView proof record
Project-declaredLean 4.8.0
Alice steps cost
alice_steps_cost
Plain-language statement
Alice makes few queries, regardless of Bob and Vera
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Alices close
alices_close
Plain-language statement
Alice produces (p,y) with p close to o.probs y with good probability
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Alices success
alices_success
Plain-language statement
Alice produces (p,y) with p close and y true with good probability, since if we condition on Alice being close she does as least as well as a close oracle.
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Bob complete
bob_complete
Plain-language statement
Honest Bob usually accepts if Alice is off by ≤ c
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Bob debate cost
bob_debate_cost
Plain-language statement
Bob makes few queries, regardless of Alice and Vera
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.