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

D>Я в свое время имел дело с "автоматическими" системами построения доказательств....

а может можно придумать высокоуровневый язык для описания доказательств теорем и вообще любых математических утверждений?
просто языки в программах типа Coq и Hol по своему "уровню" больше напоминают ассемблер. программисты(в отличии от математиков) очень хорошо думали и придумали удобные языки Программирования высокого уровня. может и для proof-assistance можно сделать высокоуровневые языки?