It's cool, but I genuinely cannot fathom why they are targeting natural language proofs instead of a proof assistant.

Natural language is a lot more, well, readable than say lean. You get a lot less intuition and understanding of what the model is attempting to do in the first place.