Методический семинар кафедры высшей математики по ИИ
МФТИ — Московский физико-технический институт ·
В среду 16 сентября в 17:20 в аудитории 113 ГК состоится методический семинар кафедры высшей математики, на котором коллеги с кафедры дискретной математики расскажут об использовании ИИ в преподавании курса ОКТЧ (Основы комбинаторики и теории чисел). Тема встречи: Курс "ОКТЧ + ИИ" (AI4Math) – опыт первого запуска Время и место: 16.09.26 17:20 - 18:30, МФТИ 113ГК Основы комбинаторики и теории чисел (ОКТЧ) - курс, проводимый с первого курса студентов ФПМИ различных направлений подготовки. Аннотация семинара ИИ-ассистенты перестали быть экзотикой в математической работе, и почти всё, что в этой области действительно работает, устроено одинаково: модель предлагает рассуждение, а проверяет его формальный верификатор – на практике Lean 4 с Mathlib. Из-за этого вопрос «что значит доказано» из философского стал рабочим, а вместе с ним появился и учебный вопрос: когда и как этому учить. Мы пробуем ответить на него с первого курса. С сентября при ОКТЧ идёт курс, где студенты осваивают этот инструментарий на материале того же задачника. Мы постараемся рассказать как устроен курс ОКТЧ, покажем как Lean проверка работает прямо в браузере, как можно использовать ИИ ассистента и при этом не потерять качество освоения материала, как задача из листка превращается в дерево вывода (а потом в код Lean). Расскажем как можно определить границу между "модель предложила" и "доказано" и что именно студент должен проверять и делать сам. Демонстрация среды — вживую. Будем рады обсудить, где такой подход применим за пределами ОКТЧ. Участники со стороны ФПМИ: - Кустов Денис Викторович, руководитель проекта, менеджер образовательного курса, к.т.н., руководитель Операционного офиса ТОП-ИИ МФТИ, доцент Образовательного центра программ топ-уровня по искусственному интеллекту - Ильинский Дмитрий Геннадиевич, доцент кафедры ДМ, лектор дисциплины ОКТЧ - Халов Андрей, Эксперт, Операционный офис ТОП-ИИ, преподаватель кафедры ДМ, основной лектор курса
В среду 16 сентября в 17:20 в аудитории 113 ГК состоится методический семинар кафедры высшей математики, на котором коллеги с кафедры дискретной математики расскажут об использовании ИИ в преподавании курса ОКТЧ (Основы комбинаторики и теории чисел). Тема встречи: Курс "ОКТЧ + ИИ" (AI4Math) – опыт первого запуска Время и место: 16.09.26 17:20 - 18:30, МФТИ 113ГК Основы комбинаторики и теории чисел (ОКТЧ) - курс, проводимый с первого курса студентов ФПМИ различных направлений подготовки. Аннотация семинара ИИ-ассистенты перестали быть экзотикой в математической работе, и почти всё, что в этой области действительно работает, устроено одинаково: модель предлагает рассуждение, а проверяет его формальный верификатор – на практике Lean 4 с Mathlib. Из-за этого вопрос «что значит доказано» из философского стал рабочим, а вместе с ним появился и учебный вопрос: когда и как этому учить. Мы пробуем ответить на него с первого курса. С сентября при ОКТЧ идёт курс, где студенты осваивают этот инструментарий на материале того же задачника. Мы постараемся рассказать как устроен курс ОКТЧ, покажем как Lean проверка работает прямо в браузере, как можно использовать ИИ ассистента и при этом не потерять качество освоения материала, как задача из листка превращается в дерево вывода (а потом в код Lean). Расскажем как можно определить границу между "модель предложила" и "доказано" и что именно студент должен проверять и делать сам. Демонстрация среды — вживую. Будем рады обсудить, где такой подход применим за пределами ОКТЧ. Участники со стороны ФПМИ: - Кустов Денис Викторович, руководитель проекта, менеджер образовательного курса, к.т.н., руководитель Операционного офиса ТОП-ИИ МФТИ, доцент Образовательного центра программ топ-уровня по искусственному интеллекту - Ильинский Дмитрий Геннадиевич, доцент кафедры ДМ, лектор дисциплины ОКТЧ - Халов Андрей, Эксперт, Операционный офис ТОП-ИИ, преподаватель кафедры ДМ, основной лектор курса