Здравствуйте, GlebZ, Вы писали:

1>>а может можно придумать высокоуровневый язык для описания доказательств теорем и вообще любых математических утверждений?
GZ>И назовем его SML!!!! (или кто-то уже делал такой?)

SML — не для "описания доказательств теорем", а для "программироваия систем доказательств".