ВИКОРИСТАННЯ МОВИ LEAN ДЛЯ ПЕРЕВІРКИ НА НЕСУПЕРЕЧНІСТЬ МАТЕМАТИЧНИХ ЗАДАЧ У НАВЧАЛЬНІЙ РЕКОМЕНДАЦІЙНІЙ СИСТЕМІ

Анотація

У статті розглянуто проблему забезпечення якості вивчення математики в умовах зростання популярності самонавчання. Запропоновано підхід на основі функційної мови Lean, що уможливлює автоматичну перевірку на точність та несуперечність даних математичної задачі та розв’язку цієї задачі. Цей підхід впроваджено в створювану рекомендаційну систему, що призначено для розв’язування математичних задач, з інтерфейсом для взаємодії та навчання кінцевих користувачів. Створена підсистема на основі мови Lean здатна виявляти потенційні помилки та суперечності в умовах задачі, а також сприяти коректному розв’язку задач.

Мову програмування Lean першочергово розроблено, щоб слугувати ефективним асистентом у доведенні теорем, через це цю мову й обрано.

Розроблено підсистему перевірки на Lean, де додано аксіоми та теореми з планіметрії, що дає змогу забезпечити інтеграцію з іншими створеними модулями системи та виконувати перевірку на несуперечність даних. Для ілюстрації потенціалу Lean використано декілька прикладів задач, що демонструють, які є переваги мови в забезпеченні точності розв’язків та виявленні помилок у математичних задачах.

У висновках  до статті підкреслено, що Lean ефективно доповнює рекомендаційну систему для розвʼязування  простих планіметричних задач, забезпечуючи не лише перевірку на несуперечність умов задачі, але й коректність розв’язків. Додатково висвітлено певні вади в мові, що ускладнюють її використання й потребують подальших досліджень та розробок для оптимізації роботи підсистеми. Порівняно з іншими підходами, як-от використання онтологій в програмі Protégé, Lean надає значні переваги в гнучкості визначення математичних моделей і виконанні нетривіальних доведень, що робить Lean потужним інструментом для підтримки якісного вивчення математики.