Coqは数学、プログラミング両方で高い水準を要求されるからな。
このスレは人集まらないだろう。
数板ではプログラムの素養がネックになるか？