AI-MO/Kimina-Autoformalizer-7B

AI-MO/Kimina-Autoformalizer-7B is a 7.6 billion parameter autoformalizer model developed by Project Numina. It specializes in translating natural language descriptions of competition-style mathematical problems into Lean 4 code, specifically generating code that ends with `by sorry`. This model is designed to assist in formalizing mathematical statements and proofs.