Математика и запись формул
От: Shmj Ниоткуда  
Дата: 30.10.19 15:02
Оценка:
Почему математики до сих пор пишут на "бумаге" и проверяют вручную, а не ввели единый по всему миру стандарт, легкий для записи и для машинного анализа?

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

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

Имх., первоые чем должны заняться математики — привести все свои знания к формальному виду. А то прямо Вавилон какой-то.
Отредактировано 30.10.2019 15:16 Shmj . Предыдущая версия . Еще …
Отредактировано 30.10.2019 15:15 Shmj . Предыдущая версия .
Отредактировано 30.10.2019 15:04 Shmj . Предыдущая версия .
Re: Математика и запись формул для компьютера
От: Sharov Россия  
Дата: 30.10.19 15:09
Оценка: :)
Здравствуйте, Shmj, Вы писали:

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


С разморозкой -- https://ru.wikipedia.org/wiki/LaTeX. На всех форумах mooc есть поддержка, т.е. люди общаются по средствам мат. формул.
Кодом людям нужно помогать!
Re[2]: Математика и запись формул для компьютера
От: Shmj Ниоткуда  
Дата: 30.10.19 15:15
Оценка:
Здравствуйте, Sharov, Вы писали:

S>С разморозкой -- https://ru.wikipedia.org/wiki/LaTeX. На всех форумах mooc есть поддержка, т.е. люди общаются по средствам мат. формул.


Это больше для графического отображения. Это как наливать новое вино в старые меха.

Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.
Re[3]: Математика и запись формул для компьютера
От: Mamut Швеция http://dmitriid.com
Дата: 30.10.19 15:26
Оценка: +3
S>Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.

0. Тебе не приходило в голову, что математическая нотация уже является формальным и вполне единым стандартом [1], который изучают, начиная со школ? И этот стандарт един для кучи наук от математики до физики до химии до биологии.

1. Потому что заманаешься писать фразы типа «сумма чисел, удовлетворяющая каким-нибудь условиям» формальным языком на латинице. Через это уже проходили до появления математической записи.

2. Для того, чтобы что-либо проверить coq'ом, надо в этот coq загрузить всю математическую теорию. Плюс не все теоремы формально проверяемы и доказуемы, хотя и используются.

[1] Да, я знаю, что далеко не все везде одинаково пишут, а в новых теориях придумывают собственную нотацию.


dmitriid.comGitHubLinkedIn
Отредактировано 30.10.2019 15:33 Mamut [ищите в других сетях] . Предыдущая версия .
Re[3]: Математика и запись формул для компьютера
От: LaptevVV Россия  
Дата: 30.10.19 15:26
Оценка: +1
S>Это больше для графического отображения. Это как наливать новое вино в старые меха.
S>Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.
Так это и есть единый для всех стандарт, сделанный еще Дональдом Кнутом чуть ли не в конце 60-х.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Re[4]: Математика и запись формул для компьютера
От: Sharov Россия  
Дата: 30.10.19 15:28
Оценка:
Здравствуйте, LaptevVV, Вы писали:

LVV>Так это и есть единый для всех стандарт, сделанный еще Дональдом Кнутом чуть ли не в конце 60-х.


Лэсли Лэмпорт же.
Кодом людям нужно помогать!
Re[5]: Математика и запись формул для компьютера
От: LaptevVV Россия  
Дата: 30.10.19 15:29
Оценка: +1
S>Лэсли Лэмпорт же.
Возможно. Просто мне попадались только книжки Кнута на эту тему.
Наверное, у нас просто Лэмпорта не переводили?
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Re[6]: Математика и запись формул для компьютера
От: Mamut Швеция http://dmitriid.com
Дата: 30.10.19 15:36
Оценка: :)
S>>Лэсли Лэмпорт же.
LVV>Возможно. Просто мне попадались только книжки Кнута на эту тему.
LVV>Наверное, у нас просто Лэмпорта не переводили?

Я надеюсь вы про (La)TeX, а не про математическую нотацию


dmitriid.comGitHubLinkedIn
Re[6]: Математика и запись формул для компьютера
От: Sharov Россия  
Дата: 30.10.19 15:37
Оценка:
Здравствуйте, LaptevVV, Вы писали:

LVV>Возможно. Просто мне попадались только книжки Кнута на эту тему.

LVV>Наверное, у нас просто Лэмпорта не переводили?

LaTeX создал Лэмпорт.
Кодом людям нужно помогать!
Re[7]: Математика и запись формул для компьютера
От: LaptevVV Россия  
Дата: 30.10.19 15:40
Оценка:
M>Я надеюсь вы про (La)TeX, а не про математическую нотацию
Я вообще про TeX. Вроде бы его создал Кнут. Но, может, я чего не знаю?
А LaTex — это же производная от TeX, не?
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Re[3]: Математика и запись формул для компьютера
От: pagid Россия  
Дата: 30.10.19 15:59
Оценка: +2
Здравствуйте, Shmj, Вы писали:

S>Почему бы не сделать единый для всех стандарт типа Wolfram Language и изучать его начиная со школ? Т.е. выкинуть все архаизмы, типа греческих букв и пр. Все писать латиницей на едином языке формальном, по типа coq. Ну и доказательства теорем принимать только в формальном виде на этом языке.


Очевидно потому что математикам и изучающим математику не нужен ни подобный язык ни теоремы в формальном виде. Традиционная запись с греческими буквами и значками для математиков куда как удобнее, и скорее программы начнут понимать такую запись и уж тем более использовать её при выводе, чем математики перейдут на запись в одну строку, без греческих букв и значков.
Re: Математика и запись формул
От: wildwind Россия  
Дата: 30.10.19 17:05
Оценка: +3
Здравствуйте, Shmj, Вы писали:

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


Элементарно, Ватсон. Математикой до сих пор занимаются только люди, а не машины. И они таки ввели единый по всему миру стандарт, легкий для записи и для человеческого восприятия, прежде всего визуального.
Re: Математика и запись формул
От: Bjorn Skalpe Земля  
Дата: 30.10.19 18:25
Оценка: :)
Здравствуйте, Shmj, Вы писали:

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


Математики давно работают в Maple
Re[2]: Математика и запись формул
От: kgd  
Дата: 31.10.19 00:10
Оценка:
Здравствуйте, Bjorn Skalpe, Вы писали:

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


BS>Математики давно работают в Maple


Да и Маткаду много лет.
Re: Математика и запись формул
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 31.10.19 12:00
Оценка: 2 (1)
Здравствуйте, Shmj, Вы писали:

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

S>Вот, есть Coq и подобные...

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