3 ms·
Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
- clbrmbr 1y agoCan 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?
- frunkp 1y agoThe 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.