Имхо, математики обязаны принять единый стандарт подачи теорем и их доказательств — только на неком формальном языке, путь там coq или любой другой. Чтобы человеческие ресурсы на проверку не тратились и была однозначность.
Так же это будет первым шагом к тому, что ИИ сам решал мат. проблемы.
Ну и такой вопрос. Что мне делать, если я хочу поработать в этом направлении, но не имею ББД? Или же не возможно это все?
