28 подписчиков
Твой хост не моделирует звёзды — он доказывает теоремы
LODA — BOINC-проект, где хосты волонтёров ищут математические формулы. Алгоритм майнинга перебирает варианты — твой компьютер проверяет и сохраняет найденные программы. Не симуляция, не перебор молекул — буквально открытие нового математического знания.
Как это работает: хост получает задание найти короткую программу, которая воспроизводит числовую последовательность из базы OEIS — каталога всех известных числовых последовательностей — для любого n.
К февралю 2026 LODA нашёл формулы для 150 000+ последовательностей — это 38% от базы OEIS (390 000+ записей). Ещё 62% ждут.
На практике: найденные программы автоматически экспортируются в LEAN — систему формальной верификации. Компьютер нашёл формулу, LEAN доказывает, что она верна для любого натурального числа.
Около минуты
28 марта