juihuichung/awakening-proofnet-runs

Awakening — ProofNet tool-use inference runs ProofNet (186 Lean 4 problems) inference outputs for the COLM 2026 paper "Awakening: minimal agentic replay recovers tool use in formal-math fine-tuned LLMs". These are the runs behind the ProofNet columns of Table 2 (tab:proofnet_main) — Goedel-Prover-V2-32B before and after post-hoc SFT on 100 / 1K / 18K Lean agentic traces, sampled 32× per problem with the LeanSearch retrieval tool available. Companion release: awakening (training… See the full description on the dataset page: https://huggingface.co/datasets/juihuichung/awakening-proofnet-runs.