#матлог #учёба #спецсеминар

Семинар «Вероятностные и субструктурные логические системы» (www.mathnet.ru/conf2533) под руководством С.Л. Кузнецова (homepage.mi-ras.ru/~sk/) и С.О. Сперанского (homepage.mi-ras.ru/~speranski/).

Время: 23 октября (четверг), 16:00
Место: МИАН, ауд. 530 + Контур.Толк

В.А. Нестеров (МФТИ)

Название:
Верифицированное вычисление асимптотик вещественных функций

Аннотация:
Вычисление асимптотик функций - одна из нетривиальных математических задач, которая, однако, под силу компьютеру. Исследования в этом направлении были начаты Г. Харди, и доведены до практического алгоритма Дж. Шекеллом в 1990 году.

В докладе я расскажу о своей имплементации алгоритма Шекелла (с некоторыми модификациями) в системе интерактивных доказательств Lean. Системы доказательств дают возможность писать доказательства на формальном языке с последующей автоматической проверкой компьютером. В своей работе я имплементировал алгоритм в виде так называемой тактики - программы, которая не только возвращает результат (например, предел функции на бесконечности), но и формальное доказательство его корректности (например, того что функция действительно стремится к найденному значению). Такая тактика, будучи использованная как подпрограмма, позволяет сократить формальные доказательства других результатов в анализе и комбинаторике.

Если планируете посетить заседание (очно или онлайн через Контур.Толк), пожалуйста, зарегистрируйтесь по ссылке в верхней части страницы семинара:

https://www.mathnet.ru/conf2533

➰ ВК