تحول در یادگیری و نگارش اثبات های صوری در ریاضیات محض: واکاوی تجارب دانشجویان در کاربست دستیار اثبات تعاملی Lean

انتقال از آموزش سنتی ریاضیات به پارادایم اثبات صوری، یکی از چالش های اساسی در آموزش عالی ریاضی محسوب می شود که دانشجویان را با شوک انتزاعی مواجه می سازد. پژوهش حاضر با هدف واکاوی کیفی تجارب دانشجویان تحصیلات تکمیلی ریاضی محض در کاربست دستیار اثبات تعاملی Lean به عنوان ابزاری نوآورانه برای ارتقای مهارت اثبات نویسی و کاهش ابهامات منطقی انجام شد.این مطالعه با رویکرد کیفی و به روش پدیدارشناسی توصیفی انجام گرفت. جامعه پژوهش شامل دانشجویان تحصیلات تکمیلی ریاضی محض دانشگاه های دولتی استان خراسان جنوبی در سال تحصیلی ۱۴۰۴-۱۴۰۵ بود. نمونه گیری به صورت هدفمند انجام شد و ۱۲ دانشجو پس از شرکت در کارگاه آموزشی فشرده کار با نرم افزار Lean، وارد فرایند صوری سازی قضایای ساختاریافته در حوزه های جبر و آنالیز شدند. داده ها از طریق مصاحبه های نیمه ساختاریافته، یادداشت های تاملی و تحلیل کدهای صوری سازی شده گردآوری گردید و با روش هفت مرحله ای کلایزی تحلیل شد.تحلیل داده ها منجر به شناسایی سه مضمون اصلی و شش مضمون فرعی گردید. مضامین اصلی عبارت بودند از: «گسست از ابهام و گذار به دقت صوری» که نشان دهنده عبور از زبان طبیعی مبهم به کدهای اصل موضوعه ای بود؛ «داربست بندی شناختی از طریق بازخورد آنی» که پویایی تعاملی، اصلاح فوری کج فهمی ها و کاهش بار شناختی را تبیین می کرد؛ و «بازتعریف هویت ریاضی دان و پارادایم اثبات» که به افزایش عاملیت فکری در کنار چالش انطباق شهود با منطق صوری ماشین اشاره داشت. نتایج نشان داد که Lean با انتقال مرجع ارزیابی از قضاوت ذهنی به بازخورد عینی ماشین، نه تنها دقت منطقی را افزایش می دهد، بلکه با ایجاد هم افزایی میان منطق صوری کامپیوتر و شهود ریاضی دان، پتانسیل بالایی در تحول برنامه های درسی ریاضیات دانشگاهی دارد.

کلیدواژه ها:

دستیار اثبات تعاملی Lean ، اثبات صوری ، آموزش ریاضیات عالی ، پدیدارشناسی ، داربست بندی شناختی.