natural language proof assistant I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english,
I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then instead of sending it to a journal to have it verified you use the proof assistant to have it verified for you.
There are programming languages like inform7 in which you program in english. I think what is needed is a set of macro's to turn the tex into, lets say, something that Coq can verify. Is there any such thing out there?
Do you think if this happens casual mathematicians will use it? or are there deeper problems that people don't use them now??

There is now a program called Coqatoo that converts Coq proofs into natural-language proofs. It may be feasible to write a translator that would convert these English proofs back into Coq, but I do not know if this has been done yet.
There are also natural-language provers that convert English text into a formal semantic representation of its meaning. For example, the ACE reasoner can prove statements that are written in Attempto Controlled English.
