stormj-UH/spivak-lean
Michael Spivak's Calculus formalized in Lean 4: every theorem and every problem of all 30 chapters and 9 appendices, in both the 3rd and 4th editions
О проекте
Формализация учебника «Calculus» Майкла Спивака на Lean 4: все теоремы и задачи 30 глав и 9 приложений 3-го и 4-го изданий, с исправлениями ошибок в книге.
Чем пригодится
- Изучить формализацию анализа на Lean 4 по главам учебника Спивака
- Проверить доказательства теорем и задач из книги в Lean без sorry и axiom
- Найти исправления ошибок в 3-м и 4-м изданиях через grep по 'Correction to Spivak'
Пересказ README моделью DeepSeek V4.1 Flash. Может ошибаться в деталях.
Почему он в тренде
- Сегодня уже 0 звёзд, к концу дня ожидается около 2.
- Репозиторию 1 день, а у него уже 2 звезды. Истории меньше двух недель, так что обычного темпа, с которым можно сравнить всплеск, у него ещё нет.
- Hacker News: «Show HN: Spivak's Calculus formalized in Lean 4 – every theorem, every problem» — 10 очков, 7 ч назад.
Звёзды по дням
Столбики — звёзды за день, линия — обычный темп. Красным — дни всплесков.
Цифры
- Всего звёзд
- 2
- Сегодня
- 0 · к вечеру ≈ 2
- Форков
- 0
- Issues и pull requests
- 0
- Наблюдателей
- 0
- Язык
- Lean
- Лицензия
- Apache-2.0
- Создан
- 26 сентября 2026
- Последний коммит
- 26 сентября 2026
Доверие к звёздам
Рост выглядит естественно: форков и обсуждений столько, сколько бывает у живых проектов, а звёзды приходят неровно, как от людей.
Это эвристики, а не приговор: судим по поведению репозитория, а не по списку звездивших.
Обсуждения на Hacker News
- Show HN: Spivak's Calculus formalized in Lean 4 – every theorem, every problem10 очков, 26 сентября 2026
Где замечен
- 27 сентября 2026Замечен на Hacker News
Поделиться
Бейдж для README
Вставьте в README — бейдж сам показывает свежую магнитуду и ведёт на эту страницу.
[](https://gitnova.dev/r/stormj-UH/spivak-lean)Похожие по описанию
-
0,8
Z3Prover/z3
Z3 — это SMT-решатель (theorem prover) от Microsoft Research с открытым исходным кодом, который проверяет выполнимость логических формул и доказывает теоремы. Используется для формальной верификации, символьного…
-
1,3
openai/NavierStokesAndEuler
Формализации на Lean 4 результатов о конечном времени разрушения решений уравнений Навье–Стокса и Эйлера, включая сертификаты для задач тысячелетия. Нужен математикам и специалистам по формальным доказательствам.