Indeed, I wonder if natural language is the right interface to this problem.

Reading earlier mathematical texts (eg, Euclid's Elements) and their "natural language" proofs reminds me that a picture is truly worth a thousand words!