Почему математики до сих пор пишут на бумаге и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа?

Вот, есть Coq и подобные. Но та же Великая Теорема (ее доказательство) до сих пор не переведено на этот формальный язык и существует только "на бумаге". Возможно он чем-то не удобен для человека, не спорю.

Есть Wolfram Language или подобные, внутрисистемные. Но это все как бы велосипеды.

Имх., первоые чем должны заняться математики — привести все свои знания к формальному виду. А то прямо Вавилон какой-то.

Почему математики до сих пор пишут на "бумаге" и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа?

Вот, есть Coq и подобные. Но та же Великая Теорема (ее доказательство) до сих пор не переведено на этот формальный язык и существует только "на бумаге". Возможно он чем-то не удобен для человека, не спорю.

Есть Wolfram Language или подобные, внутрисистемные. Но это все как бы велосипеды.

Имх., первоые чем должны заняться математики — привести все свои знания к формальному виду. А то прямо Вавилон какой-то.