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

Я думаю, поэтому математики это не принимают. Им ещё нужна свобода давать определения всякие разные, сначала, может быть, ошибочные.

Я не понял при чём тут операционка. Все эти соображения обсуждались гораздо глубже действующими математиками на круглом столе, запись которого я привёл выше.

Я в процессе прослушивания. Но вот, они основную проблему обговаривают: когда математик понимает, как это всё забить в theorem prover, он уже доказал всё, что ему нужно, и он уже пишет статью :) Наверное, это всё может взлететь, если формализации уже известных теорем будут признавать за публикации и платить за это. Но много ли математиков захотят этим заниматься?

Увидим. Некоторые, очевидно, хотят.

Кроме того, "что такое математика" и "как ей заниматься" - как они говорят - moving target. Если через 20 лет бОльшая часть математиков перейдёт на формализацию всего в пруверах - это просто станет нормой. 🤷‍♀️

Насчёт "когда математик понимает, как это всё забить в theorem prover, он уже доказал всё, что ему нужно" - это просто сейчас доминирует такой режим работы просто потому что в университете математиков учат доказывать на бумаге, а не в прувере.

Кто плотно освоил прувер - начинает "заниматься математикой" сразу в нём.

Математики занимаются математикой на доске. Без доски, без рисунков, без диалога большинству будет крайне тяжело это делать. Ну. Таковы мои наблюдения за коллегами. В этом проблема, повторюсь. К тому моменту, когда теорема доказана, она уже доказана. Формализация ничем не поможет (ну, если за неё не будут давать премию).

Математики бывают разные. Разделы математики тоже разные. Есть простор для разных подходов. 😊

Это, конечно

А есть какой-то список участников? Если это матлогика, то они очень отдаленное отношение имеют к остальной математике, насколько я понимаю.

В начале озвучивают список участников. Вроде, не только логики. Вообще, интересный диалог

коллеги, вопрос терминологический

"литерал" в контексте лексического анализа как-нибудь надо переводить?

например, литерал строки при разборе кода на Си ("bla bla bla") или текстового символа('c')?

"Строковый литерал" вроде норм

вполне нормальный термин

ок, спасибо

можно заменить словом «константа», если подобные англицизмы приемлемы