LeanSearch v2: Recupero Globale delle Premesse per la Dimostrazione di Teoremi in Lean 4

LeanSearch v2 è un framework di recupero a due modalità progettato per il recupero globale delle premesse nella dimostrazione di teoremi in Lean 4. La sua modalità standard sfrutta un corpus Mathlib informalizzato gerarchicamente insieme a una pipeline di embedding e riordinamento, raggiungendo prestazioni leader nel recupero a singola query (nDCG@10 di 0,62, superando il sistema successivo con 0,53) senza richiedere messa a punto specifica del dominio. Nel frattempo, la modalità di ragionamento si concentra sul recupero globale delle premesse attraverso cicli iterativi di abbozzo-recupero-riflessione. Questo sistema identifica efficacemente una raccolta dispersa di lemmi di libreria per dimostrazioni succinte, un'area non adeguatamente affrontata dagli strumenti esistenti come i motori di ricerca semantica e i sistemi di selezione delle premesse. Per la valutazione, è stato utilizzato un benchmark composto da 69 query relative a teoremi Mathlib a livello di ricerca.