The work being carried out on the development of Ukrainian and Russian versions of the ForTheL formal natural language, which is the input language of the system for automated deduction SAD (http://nevidal.org/sad.en.html) and simulates the structure of sentences of ordinary English, is described. The implementation of these versions will allow to do a remote access to the SAD system for solving tasks of theorem proving and mathematical text verification for users who speak only one of the three languages (English, Russian or Ukrainian), which confirms a perspectivity of providing human mathematical activity with a computer support in languages that, on the one hand, are formal, but, on the other hand, are as close to the languages used by people in their daily practice as possible.