Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
huggingface.coCan I start with a natural language description of the theorem to be proven and the model will automatically formalize it? And can I get a natural language interpretation of the Lean proof in case of success? --- I'm thinking of working through Elements of Abstract Algebra with this, but not sure if it has such general applicability?
The model does well on highschool competition maths. Problems in the "Set Theory" and "Natural Numbers" chapters of Elements of Abstract Algebra may be doable with Kimina-Prover, nothing beyond because it doesn't know Sylow theorem etc. and hasn't used these objects with Lean 4 in practice.
You can start with a natural language description of the theorem: demo.projectnumina.ai and an autoformalizer will generate the formal statement. It's an additional click of a button to have it attempt to prove it.
For natural language interpretation of Lean proofs, the current LLMs (o4-mini-high, Claude 4, Gemini 2.5 Pro) do a decent job of walking you through.