Source-pinned research
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 18 research declarations. Search 10,000 more complete Mathlib declarations.
18 results
Clear filtersbobs_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.
Source project: debate
Person-level attribution pending.
completeness_p
Plain-language statement
Completeness for any valid parameters
Source project: debate
Person-level attribution pending.
completeness'
Plain-language statement
Alice wins the debate with good probability
Source project: debate
Person-level attribution pending.
debate_eq_transposed
Plain-language statement
The transposed formulation of debate is the same
Source project: debate
Person-level attribution pending.
evil_alices_lies
Plain-language statement
Evil Alice produces a close true trace with low probability, since by remaining close she looks like a close oracle.
Source project: debate
Person-level attribution pending.
evil_bobs_lies
Plain-language statement
If Alice is good, the probability of false is low
Source project: debate
Person-level attribution pending.