Goedel-Formalizer-V2-32B: Advanced Math Autoformalization

Goedel-Formalizer-V2-32B is a 32 billion parameter model developed by Goedel-LM, specifically engineered for the autoformalization of informal mathematical problem statements into Lean 4 code. This model is a core component of the Goedel-Prover-V2 project, aiming to bridge the gap between natural language math problems and formal verification systems.

Key Differentiators & Capabilities

• "Think Before Generating" Mechanism: A unique feature that allows the model to process and reason about the informal statement before generating the Lean 4 output, leading to substantially higher accuracy compared to prior formalizers.
• High Formalization Success Rate: Achieved a success rate of 226 out of 300 informal statements on an internal evaluation set derived from Omni-MATH, outperforming models like Kimina-formalizer-8B (161/300).
• Direct Lean 4 Output: Generates ready-to-use Lean 4 formal statements, streamlining the process for formal verification and theorem proving.

Ideal Use Cases

• Automated Theorem Proving: Generating formal Lean 4 statements from natural language descriptions to be used with automated theorem provers.
• Mathematical Research: Assisting mathematicians in formalizing their conjectures and proofs.
• Educational Tools: Creating tools that help students understand the formalization process of mathematical concepts.