Library Card: Automated Repository Knowledge Interface for Lean Theorem Proving

Automated theorem proving (ATP) in large Lean repositories requires both retrieving relevant premises and providing repository-specific information that supports their effective use. Premise retrieval is central to repository-aware theorem proving, but premise availability and proof-time context are often evaluated jointly. To address this, we introduce Library Card, an automated repository knowledge interface for Lean theorem proving. Library Card automatically constructs and organizes repository-specific knowledge, then uses it to independently control the premises available for selection and the context provided around selected premises. This separation enables a controlled study of whether proving performance is limited by finding additional premises or by using available repository knowledge more effectively. On a 50-theorem benchmark from Optlib, the baseline formal-plus-semantic retriever recovers all 37 observable earlier-same-file source-proof premise occurrences at $K=50$, while Card-based expansion rarely changes the selected premise set. With selected premises and their order fixed, the observed solve rate is 54% with rich context versus 44% with compact context, although the paired difference is statistically inconclusive. Additional controls show no aggregate advantage for the tested structured or compiled representations. These results suggest that when the evaluated retrieval budget already covers the observable premises in scope, progress may depend less on expanding candidate availability and more on how repository-specific knowledge is provided to the prover. Our source code and data are available at https://anonymous.4open.science/r/Library-Card.