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

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

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

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

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

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

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

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

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

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