Из математической теории в проверяемую библиотеку за 9 месяцев

Задача

Арифметика с плавающей точкой молча теряет информацию. Сумма [1e16, 1, −1e16] даёт 0, значимые разности схлопываются в ложные нули, а деление на ноль бросает исключение вместо того, чтобы стать частью модели данных. В финансовых и научных расчётах исправления размазаны по частным заплаткам. Мы поставили задачу сделать арифметику, где потеря точности и особые случаи явны, структурированы и проверяемы, а заявленные свойства доказаны и измерены.

Что сделали

• Собрали ядро на основе Абсолютной Компенсационной Теории (ACT): каждая операция возвращает результат и явную компенсацию, а особые случаи становятся структурированными состояниями с политиками обработки.
• Поверх ядра добавили компенсированную линейную алгебру (GEMM, QR, SVD), оптимизаторы для машинного обучения с обёрткой для PyTorch, финансовый журнал проводок и интеграции с NumPy и pandas.
• Доказали публичные теоремы на Lean 4 и Mathlib. Сборка формального проекта подтверждает, что пропусков (sorry) нет и используются только три стандартные аксиомы Lean. Доказана алгебра модели над вещественными числами, поведение float64 не формализовано.
• Ввели правило: каждое численное утверждение в документации привязано к воспроизводимому бенчмарку и пересчитывается в том же изменении. Проигрыши публикуем рядом с выигрышами: точные операции медленнее обычных, и это тоже измерено.
• Выпустили публичный релиз на PyPI (сейчас версия 1.1.0) под лицензией AGPL-3.0 или коммерческой, с конвейером публикации пакета. В разрабатываемой версии проходят 870 тестов (на 05.10.2026), покрытие строк 76 %.

Результат

1,0 вместо 0,0

сохранён остаток суммы [1e16, 1, −1e16], который float теряет; воспроизводимый бенчмарк генерируется скриптом из репозитория

6 из 6

сценариев опубликованного бенчмарка, где точное ядро скалярного произведения совпало с точным эталоном; numpy.dot совпал в 0 из 6. Ядро на C на PyPI пока не выпущено, а сценарий, где слагаемые взаимно уничтожаются, построен специально

0 пропусков

в доказательствах алгебры модели на Lean 4 + Mathlib (0 sorry), используются только три стандартные аксиомы; поведение float64 не формализовано

9 месяцев

от первого коммита до первого стабильного релиза на PyPI, по истории тегов и коммитов репозитория (актуальная версия 1.1.0)

Услуги

Другие кейсы