2025
miniCTX: Neural Theorem Proving with (Long-)Contexts
ICLR 2025oral
Real-world formal theorem proving often depends on a wealth of context, including definitions, lemmas, comments, file structure, and other information. We introduce $\texttt{miniCTX}$, which tests a model's ability to prove formal mathematical theorems that depend on new context that is not seen dur…