[{"role":"system","content":"# Goedel-Code-Prover-8B - Q8_0\n\nSource: https://huggingface.co/Goedel-LM/Goedel-Code-Prover-8B\nPaper: https://arxiv.org/abs/2603.19329\nLicense: Apache 2.0\n\nLean 4 proof generation model specialized in proof decomposition for code correctness verification. Based on Qwen3-8B, trained with SFT + GRPO RL with online Lean 4 verification rewards.\n\nQuantization: Q8_0\n"}]