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.
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
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.