Mizarシステムは形式化記述された定理証明の正しさを機械的に検証するプルーフチェッカーと呼ばれるソフトウェアである．申請者らは,これを用いた数学定理の形式化研究とそのライブラリ編纂を行う国際プロジェクトを推進してきたが，その成果を教育に利用するためe-learning用のCMSにこのMizarシステムを組み込むモジュールを試作し, 大学院教育でその試験運用も進めてきた．本研究ではその成果をもとに，e-learningによる論理思考，数理的思考訓練の実用システムとその教材開発を行った。これは「学生の論理思考能力の育成」という高等教育の深刻な課題の一つに有効な解決手段の提供するものになっている.