Почему математики до сих пор пишут на "бумаге" и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа?
Вот, есть Coq и подобные. Но та же Великая Теорема (ее доказательство) до сих пор не переведено на этот формальный язык и существует только "на бумаге". Возможно он чем-то не удобен для человека, не спорю.
Есть Wolfram Language или подобные, внутрисистемные. Но это все как бы велосипеды.
Имх., первоые чем должны заняться математики — привести все свои знания к формальному виду. А то прямо Вавилон какой-то.
Здравствуйте, Shmj, Вы писали:
S>Имх., первоые чем должны заняться математики — привести все свои знания к формальному виду. А то прямо Вавилон какой-то.
Здравствуйте, Sharov, Вы писали:
S>С разморозкой -- https://ru.wikipedia.org/wiki/LaTeX. На всех форумах mooc есть поддержка, т.е. люди общаются по средствам мат. формул.
Это больше для графического отображения. Это как наливать новое вино в старые меха.
Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.
S>Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.
0. Тебе не приходило в голову, что математическая нотация уже является формальным и вполне единым стандартом [1], который изучают, начиная со школ? И этот стандарт един для кучи наук от математики до физики до химии до биологии.
1. Потому что заманаешься писать фразы типа «сумма чисел, удовлетворяющая каким-нибудь условиям» формальным языком на латинице. Через это уже проходили до появления математической записи.
2. Для того, чтобы что-либо проверить coq'ом, надо в этот coq загрузить всю математическую теорию. Плюс не все теоремы формально проверяемы и доказуемы, хотя и используются.
[1] Да, я знаю, что далеко не все везде одинаково пишут, а в новых теориях придумывают собственную нотацию.
S>Это больше для графического отображения. Это как наливать новое вино в старые меха. S>Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.
Так это и есть единый для всех стандарт, сделанный еще Дональдом Кнутом чуть ли не в конце 60-х.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Здравствуйте, LaptevVV, Вы писали:
LVV>Возможно. Просто мне попадались только книжки Кнута на эту тему. LVV>Наверное, у нас просто Лэмпорта не переводили?
M>Я надеюсь вы про (La)TeX, а не про математическую нотацию
Я вообще про TeX. Вроде бы его создал Кнут. Но, может, я чего не знаю?
А LaTex — это же производная от TeX, не?
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Здравствуйте, Shmj, Вы писали:
S>Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.
Очевидно потому что математикам и изучающим математику не нужен ни подобный язык ни теоремы в формальном виде. Традиционная запись с греческими буквами и значками для математиков куда как удобнее, и скорее программы начнут понимать такую запись и уж тем более использовать её при выводе, чем математики перейдут на запись в одну строку, без греческих букв и значков.
Здравствуйте, Shmj, Вы писали:
S>Почему математики до сих пор пишут на "бумаге" и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа?
Элементарно, Ватсон. Математикой до сих пор занимаются только люди, а не машины. И они таки ввели единый по всему миру стандарт, легкий для записи и для человеческого восприятия, прежде всего визуального.
Здравствуйте, Shmj, Вы писали:
S>Почему математики до сих пор пишут на "бумаге" и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа?
Здравствуйте, Bjorn Skalpe, Вы писали:
S>>Почему математики до сих пор пишут на "бумаге" и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа?
BS>Математики давно работают в Maple
Здравствуйте, Shmj, Вы писали:
S>Почему математики до сих пор пишут на "бумаге" и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа? S>Вот, есть Coq и подобные...
Coq и подобные работают в парадигме конструктивной математики, там можно доказывать и проверять машиной те утверждения, где доказательство строится конструктивно, из конечных сущностей. Но в обычной математике очень много теорем и определений неконструктивных, опирающихся на принцип исключения третьего ("доказательство от противного") и на пределы бесконечных последовательностей. Многие теоремы или невозножно проверить такими пруф-чекерами, или иногда возможно, но требуется очень много скучной ручной работы по разъяснению деталей, многим математикам неохота, некогда и обычно незачем этим заниматься.