AI-MO
3 models in Artifacts Logshuggingface.co/AI-MO
Kimina-Prover-72B09 Jul 2025
72BMIT (Qwen2.5 Base)115 · 30d
A Lean 4 generation model for proofs, built on top of Qwen2.5 72B.
Kimina-Prover-Preview-Distill-7B10 Apr 2025
7BApache-2.0195 · 30d
A model from Moonshot AI specialized in proving math problems by formalizing them into Lean. They also release the Autoformalizer, which is capable of converting natural language into Lean 4 code. This is helpful for systems like AlphaProof.
NuminaMath-7B-TIR04 Jul 2024
373 · 30d
A fine-tune of DeepSeek-Math that won the math competition I mentioned above. Domain-specific models are getting serious.