Paper recorded by Signals 4 on 2026-10-15 in cs.LG. Abstract reproduced from arXiv; link to the original below.
Published 2026-10-15 on arXiv · recorded by Signals 4 on 2026-10-16
Category: cs.LG · 机器学习 · first seen 2026-10-16
Retrieving relevant lemmas is crucial for formal theorem proving, enabling provers to build machine-checkable proofs from established mathematical results. Recent retrieval systems match library declarations to a target theorem or its intermediate proof steps, but make limited use of multi-hop dependencies among declarations. These dependencies can reveal supporting lemmas that are not necessarily