Помощник для справки только для математики

Question

Большинство помощников по доказательству являются функциональными языками программирования с зависимыми типами. Они могут проверять программы/алгоритмы. Я заинтересован, вместо этого, в помощнике доказательств, подходящем для математики и только (например, исчисления). Вы можете порекомендовать его? Я слышал о Mizar, но мне не нравится, что исходный код закрыт, но если он лучше всего подходит для математики, я буду использовать его. Насколько хорошо новые языки, такие как Agda и Idris, подходят для математических доказательств?

Answer 1

Coq имеет обширные библиотеки, охватывающие реальный анализ. Различные события приходят на ум:

• standard library и проекты здания на нем, например, как ныне несуществующей coqtail проекта [1] (с широким охватом степенных рядов и совсем немного работы с комплексными числами) или более последнее время coquelicot. Все они полагаются на аксиоматическое определение реалов presented here.

• Более конструктивный подход предоставляется проектом the C-CoRN, который начинается с фактического построения реалов.

Другой способ решения проблем состоит в том, чтобы обратиться к нестандартному анализу. Это то, что делали люди, использующие ACL2.

Для более общего вида поля, вы должны, вероятно, прочитать this survey paper людьми, участвующими в проекте coquelicot.

[1] полное раскрытие: я был вовлечен в этот проект