Goedel-LM/Goedel-Prover-V2-8B

Goedel-Prover-V2-8B is an 8 billion parameter language model developed by Goedel-LM, specifically designed for automated formal proof generation. It achieves state-of-the-art performance on theorem proving benchmarks like MiniF2F, matching larger models while being significantly smaller. This model excels at generating and self-correcting formal proofs, making it highly effective for mathematical reasoning and formal verification tasks.