Leftover Hash Lemma
The leftover hash lemma and the tightness of its randomness-extraction bound.
| Status | Statement | Tags |
|---|---|---|
|
LHL extraction, public seed Proven, and the statement is now formalized in Lean with an AI match check: the public-seed bound holds with a concrete constant, but the proof itself is still only informal (PDF), unreviewed, and unformalized. 6 open |
Leftover Hash LemmaRandom Oracle ModelRandomness Extractionromtight-boundresearch-solvedadaptation (ai) |
No matching items