现实世界中的形式化定理证明通常依赖于大量上下文信息，包括定义、引理、注释、文件结构和其他信息。我们引入了 miniCTX，它测试模型证明形式化数学定理的能力，这些定理依赖于训练期间未曾见过的新的上下文信息。miniCTX 包含来自真实 Lean 项目和教科书的定理，每个定理都与一个可能包含数万个标记的上下文相关联。模型的任务是在访问定理库中的代码（其中包含证明所需的上下文）的情况下证明一个定理。作为 miniCTX 的基线，我们测试了微调和提示方法，这些方法将定理证明与之前的上下文联系起来。这两种方法都显著优于仅依赖于状态信息的传统方法。我们发现，这种利用上下文的能力在之前诸如 miniF2F 之类的基准测试中并未体现出来。除了 miniCTX，我们还提供了 ntp-toolkit 用于自动提取和注释定理证明数据，使将新项目添加到 miniCTX 中变得容易，以确保上下文在训练期间未曾见过。miniCTX 为神经定理证明器提供了一个具有挑战性和现实性的评估。