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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.

All topics

Showing 1,129 to 1,134 of 2,569 results.

Project-declaredLean 4.32.0

Knowledge Soundness

Fischlin.knowledgeSoundness

Mathematical statement

Knowledge soundness of the Fischlin transform via online (straight-line) extraction (Fischlin 2005, Theorem 2). If the Σ-protocol is specially sound with unique responses, then for any cheating prover making at most Q hash queries, the probability that the verifier accepts but the online extractor fails to recover a valid witness is at most `(Q + 1) · (...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0

Run m Of Fn query hit

Fischlin.run_mOfFn_query_hit

Mathematical statement

Simulating the verifier's Fin.mOfFn of random-oracle re-queries on a cache that already stores every re-queried record is deterministic: each query is a cache hit returning the stored value, leaving the cache untouched. The result is the pure product of the per-repetition outputs f i (hash i), where hash i is the value cached at record i.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record

Project-declaredLean 4.32.0