![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Quote of the Day: Groupoids
Formulating mathematical reasoning in a language precise enough for a computer to follow meant using a foundational system of mathematics not as a standard of consistency to establish a few fundamental theorems, but as a tool that can be employed in everyday mathematical work. There were two main problems with the existing foundational systems, which made them inadequate.
- Firstly, existing foundations of mathematics were based on the languages of predicate logic and languages of this class are too limited.
- Secondly, existing foundations could not be used to directly express statements about such objects as, for example, the ones in my work on 2-theories.
...
The greatest roadblock for me was the idea that categories are “sets in the next dimension.” I clearly recall the feeling of a breakthrough that I experienced when I understood that this idea is wrong. Categories are not “sets in the next dimension.” They are “partially ordered sets in the next dimension” and “sets in the next dimension” are groupoids.
-- V. Voevodsky. https://www.ias.edu/ideas/2014/voevodsky-origins
no subject
And I now do my mathematics with a proof assistant. I have a lot of wishes in terms of getting this proof assistant to work better, but at least I don’t have to go home and worry about having made a mistake in my work. I know that if I did something, I did it, and I don’t have to come back to it nor do I have to worry about my arguments being too complicated or about how to convince others that my arguments are correct. I can just trust the computer. There are many people in computer science who are contributing to our program, but most mathematicians still don’t believe that it is a good idea. And I think that is very wrong.
"
no subject
no subject
А почему его массово не понимают, не понимаю.
Какая-то инерция мышления, и у математиков, и у программистов.
no subject
no subject
Да и черновики никто не запрещает рисовать хоть бы и на салфетках.
А переход от бумаги к символам в вычислительном устройстве во времена, когда у каждого смартфон в кармане, - не большая беда.
Например, чертежи для материальной инженерии никто на бумаге с кульманом давно не рисует.
Главное, это дает большую на порядок уверенность в результате.
"Так выпьем же за кибернетику!" (с)
no subject
no subject
и да, и нет.
думать о задаче надо по-старому, но выражать придуманное придется новыми средствами.
больше усилий по части выражения, но и результат более надежный.
что будет дальше, трудно предсказать.