این مقاله توصیه می کنه که استادها در تدریس از Lean استفاده کنند. می گه این کار باعث می شه که دانشجو تمام مراحل منطقی اثبات رو بفهمه وجزییات اون رو بررسی کنه.می گه دانشجوها معمولا اثبات ها رو حفظ می کنند. استفاده از Lean باعث می شه که بفهمند چرا بعضی جاها چیزی که نوشتند کار نمی کنه و این به درک عمیق از اثبات منجر می شه. اشاره می کنه به جمله تائو که از نقش
Interactive Theorem Prover, ML,...
در ریاضیات سال های می گه.
پنج مشکل در آموزش و درک اثبات این ها هستند:
۱.چرا اثبات مهمه اصلا؟
۲. دانشجوها اثبات ها رو حفظ می کنند و ایده ها رو درک نمی کنند.
۳. درک یکسانی از اثبات وجود نداره.
۴. دانشجوها توان یا اعتماد به نفس بررسی درستی اثبات رو ندارند. هر چی در جزوه و کتاب نوشته یا استاد می گه رو درست می دونند.
۵. بلد نیستند اثبات رو بشکنند به بخش های کوچک تر
Teaching Mathematics with Lean: Interactive Theorem Provers in the Classroom