Can 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 · 1d ago
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.
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.