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

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