Hi: It is good to hear you after such time. I would like to know more about it. It is a pity that nobody in Russia is interested in Mizar. We cooperate mostly with Japan and China. All the best, Andrzej Cytowanie "PbIKOB__B.B." <rykov2000@mail.ru>:
Quite unexpectedly I attended a report here in Moscow about
computer theorem proving today.
Our mathematician Beklemishev (in his 30s) told about Coq based
project, his research and some review (at the beginning - of course)
He mentioned Mizar among 5-6 best projects.
If you want details - I could write a bit more.
Happy Easter!
Vladimir Rykov, PhD in Computational Linguistics,
MOSCOW
//rykov.narod.ru/
Tel +7-903-749-19-99
ďÔ×ĹŢÁĘÔĹ ÎÁ vlad.rykov@gmail.com