The System for Automated Deduction can check proof texts both in English and Russian if I remember correctly: SAD

Translating keywords is of course an easy task, but it'd be interesting to see if there are more fundamental differences in how mathematics is presented in different languages. Most researchers in theorem proving are logicians by training, and logic is usually considered to be universal, but it's probably worthwhile to take insights from linguistics into account when designing languages to interact with theorem provers.

The System for Automated Deduction can check proof texts both in English and Russian if I remember correctly: SAD

Translating keywords is of course an easy task, but it'd be interesting to see if there are more fundamental differences in how mathematics is presented in different languages. Most researchers in theorem proving are logicians by training, and logic is usually considered to be universal, but it's probably worthwhile to take insights from linguistics into account when devising languages for theorem provers.