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.
All projects
Standalone Lean project
debate
Formalizing stochastic doubly-efficient debate
52indexed declarationsLean 4.8.0mathlib@b5eba5954288commit de3a6e500ae1Apache-2.0Repository Versions and build evidence
Flagship declarations
Start with the mathematical results
View 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.
Project index
More declarations
Showing 8 of 46 additional declarations. Use project search for the complete index.
Project-declaredLean 4.8.0
Bob sound
bob_sound
Plain-language statement
Honest Bob usually rejects if Alice is off by ≥ s
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Bob steps cost
bob_steps_cost
Plain-language statement
Bob makes few queries, regardless of Alice and Vera
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Bobs catches
bobs_catches
Plain-language statement
If Alice lies about probabilities by more than b, Bob usually catches Alice in a lie
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Bobs safe
bobs_safe
Plain-language statement
If Honest Bob rejects, Vera usually complains. The error probability is higher if Bob does complain, though, so we use an expectation over vera_score.
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Chernoff count abs le
chernoff_count_abs_le
Plain-language statement
Chernoff symmetric bound
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Chernoff count le
chernoff_count_le
Project documentation
Weak Chernoff's theorem for the Bernoulli case
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Chernoff estimate abs le
chernoff_estimate_abs_le
Plain-language statement
Chernoff symmetric bound for estimate
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Chernoff le count
chernoff_le_count
Plain-language statement
Chernoff lower bound
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.