Indeed, I wonder if natural language is the right interface to this problem. Reading earlier mathematical texts (eg, Euclid's Elements) and their "natural lang

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!