ОГОЛОШЕННЯ

Лоран: теореми аналізу

Сучасні системи доведень, такі як Coq і Lean, є справжніми помічниками математиків, коли йдеться про формальну перевірку теорем чи роботу зі складними структурами. Але в таких галузях, як числення, функціональний аналіз чи теорія розподілів Лорана Шварца, ці універсальні інструменти часто використовують набір готових тактик — linearith, norm_num, тактики для спрощення виразів ring і field, continuity і limit — щоб впоратися з особливостями аналізу. Хоча це працює, такі методи здаються відірваними від того, як математики мислять на папері. Саме тому з’явилася ідея створити — спеціалізований інструмент для доведень, який би відображав дух оригінальної математики в цих галузях.

Розробка почалася з простого питання: чому б не зробити систему, яка ближча до природного математичного мислення? У Coq і Lean поняття міри, множин чи топології часто заховані в записи чи складні залежні типи, що ускладнює роботу. У новому підході ці ідеї стали основою — простими й ефективними елементами, які легко використовувати. — це спроба повернути математиці її інтуїтивність, водночас зберігаючи формальну строгість. Ось як це вдалося реалізувати.

Квантори

Будь-яка система доведень починається з типу даних, і не виняток. Усе будується на залежних типах Пі (функції) та Сигма (пари), а також кванторах узагальнення і існування. Ці базові елементи знайомі з Coq чи Lean, але тут вони особливі: їх зробили такими, щоб працювати з аналізом було зручно й зрозуміло. Наприклад, коли ви пишете "для всіх x у дійсних числах", це не просто формальність — це частина системи, яка відчувається як справжня математика.

Типи

Далі йдуть базові типи, які потрібні для числення та аналізу: натуральні (), цілі (), раціональні (), дійсні (), комплексні (), кватерніони (), октоніони () та вектори розмірності n (). У більшості систем ці типи додають через бібліотеки, але в вони вбудовані з самого початку. Завдяки цьому обчислення стають швидшими, а робота з границями чи похідними — простішою.

Теорія множин

Теорія множин — це фундамент математики, і в вона не просто додаток. Множини тут — це базові об’єкти з операціями об’єднання чи перетину, які вбудовані в саму систему. Наприклад, можна легко визначити множину позитивних дійсних чисел:

let set_a : exp =
  Set (Lam ("x", Real,
    RealIneq (Gt, Var "x", Zero)))

Це , а система одразу знає, як із цим працювати.

Теорія міри

Міра — ключ до функціонального аналізу й розподілів, і в вона вбудована в ядро системи. Це базовий елемент із готовими властивостями, як-от адитивність чи повнота. Завдяки цьому доведення про інтеграли чи збіжність стають швидшими й природнішими.

Аналіз

Найголовніше в — це примітиви для роботи з теоремами математичного аналізу: границі, похідні, інтеграли, ряди. Завдяки примітивам тут можна визначити границю послідовності безпосередньо:

let sequence_a : exp =
    Lam ("n", Nat,
      RealOps (Div, One,
        NatToReal (Var "n")))

Послідовність із границею , яку система може довести автоматично.

Теорія розподілів

Для теорії розподілів — із тестовими функціями та узагальненими похідними — усе виглядає так, ніби пишеш підручник. Система підтримує інтеграли, як-от , і простори типу .

Що далі?

як мінімальний продукт не прагне замінити Coq чи Lean. Це інструмент для тих, хто хоче працювати з численням і аналізом так, як це робили великі математики. Проєкт уже живе на GitHub в репозиторії groupoid/laurent, і кожен може долучитися до його розвитку. У майбутньому ми додамо більше тактик, покращимо швидкість і доведемо ключові теореми аналізу та розподілів. Мета — зробити математику інтуїтивною, точною і красивою.