There are declarative systems like Mizar and Isar that do take something a bit closer to natural language proof text as input. Outputing actual text in natural language is just an exercise in pretty-printing (and of course the system must know and work with the natural-language name for every object and statement you're working with, otherwise the output gets clunky).