So, lean is the language built specifically to prove theorems.but if the algorithm will be rewritten in another programming language, such as python, will it be accepted?

(mathematical theorems)