Formalizing the Hidden Number Problem in Isabelle/HOL
Formalizing the Hidden Number Problem in Isabelle/HOL
Sage Binder,Eric Ren,Katherine Kosaian
2025 · DOI: 10.4230/LIPIcs.ITP.2025.23
International Conference on Interactive Theorem Proving · 0 Citations
TLDR
This work formalizes the hidden number problem, as introduced in a seminal work by Boneh and Venkatesan in 1996, in Isabelle/HOL, and makes use of an instance of Babai’s nearest plane algorithm, which solves the approximate closest vector problem.