Жежерун, ОлександрКривошея, Олександр2026-08-272026-08-272026https://ekmair.ukma.edu.ua/handle/123456789/41002Магістерську роботу присвячено розробці та дослідженню інтелектуальної програмної системи автоматизованої перевірки розгорнутих геометричних міркувань учнів 7–9 класів на основі фреймворку Lean 4 та великих мовних моделей. Об’єкт дослідження: процеси автоматизованої перевірки правильності математичних викладів у інтелектуальних навчальних середовищах. Предмет дослідження: методи та програмні інструменти інтеграції середовища Lean у рекомендаційну систему для перевірки геометричних доведень. Мета дослідження: розробити та дослідити архітектуру програмного додатка, який використовує ядро Lean для перевірки геометричних міркувань учнів, діагностує рівень їхньої підготовки та надає адаптивні рекомендації на основі виявлених прогалин.ukLean 4перевірка математичних міркуваньнейро-символічна інтеграціяформальна верифікаціявеликі мовні моделіпланіметріяформувальне оцінюваннямагістерська роботаOther