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.