3 ms·
> Mathematical ideas, even simple ideas, are often hard to transplant from mind to mind.... Our understanding frequently deteriorates as well... The experts in
by ke88y 3y ago
> Mathematical ideas, even simple ideas, are often hard to transplant from mind to mind.... Our understanding frequently deteriorates as well... The experts in a subject retire and die, or simply move on to other subjects and forget.... In short, mathematics only exists in a living community of mathematicians that spreads understanding and breaths life into ideas both old and new.
One of the great things about software is that you don't need a living community that holds every bit of every code base in their head. You can rely on abstraction boundaries, and then jump down rabbit holes only if and when necessary.
I really wonder how the work of Mathematics will change once computer-encoded proofs become mainstream. I have to imagine that will happen within the next generation or two -- as soon as the automation becomes more helpful than the hindrance of formality.
- Ericson2314 3y agohttps://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib https://1lab.dev/ https://1lab.dev/ You can watch the next generation, or participate, right now.
- robryk 3y agoI think you're missing his point. He does acknowledge that statements of facts and their proofs can be easily communicated, but claims that the understanding their discovery was a side effect of cannot be communicated easily. This is not affected by having a better way to express facts and their proofs.
- ke88y 3y agoNo, I get his point. I think the transmission of knowledge and insight and clarity works very differently for executable artifacts than for artifacts written in natural language. > This is not affected by having a better way to express facts and their proofs. But it is if those expressions are possible to interact with and use through not only conceptual abstraction but also procedural abstraction. With good proof automation? Maybe you can interact and play with ideas through many layers of automation-enabled abstraction. Maybe you have a tactic or ATP procedure that uses a lemma in clever ways without you even knowing it exists, and only after building on that edifice for years do you bother to dig in and understand what the proof automation is even using. Mind you: not what the lemma means or how it's proven or the underlying historical development of ideas, but that it even exists. Maybe you never dig in and realize it exists. Maybe you use these new theorems and proofs -- discovered only through extremely essential and clever use of a critical lemma you don't even know that you are using -- to do something useful in the world. That can't happen today; not really. It would take very powerful proof automation for this world to exist. Code and books are very different things.
- deleted 3y ago[deleted]