Conjecture-Gym：生成 Lean 验证定理语料的 PolyForge 与用其训练的 nano-prover
GitHub 开源项目 Conjecture-Gym 包含两部分：PolyForge 通过符号前向推导生成图论猜想，仅当 .lean 文件通过 Lean 4 kernel 编译（无 sorry、仅标准公理）时才写入语料，全程无 LLM 参与；下游对小型代码 LLM 做 LoRA SFT 微调，并用真实 Lean pass@k 评分。两阶段仅通过 output/train_corpus.jsonl 文件连接，语料按公式去重、持续累积。