4 ms·
> Now that's a fine thing in a computer language -- and there are philosophers who say mathematical truth is no more than computation. But mathematical notation
by pwdisswordfish 10y ago
> Now that's a fine thing in a computer language -- and there are philosophers who say mathematical truth is no more than computation. But mathematical notation is for humans to talk about things that have meanings that humans can understand.
Then how come an unfamiliar piece of source code is easier to follow than a mathematics paper using unfamiliar notation?
You can look up the definition of each function and learn precisely what it does, without ambiguities. You can open up a debugger and trace every step of the algorithm. Source code tends to be formatted to emphasise its division into units that can be analysed separately. Even if the code uses a framework you don't recognise, you can probably understand some of the underlying logic just fine, thanks to a consistent syntax and (often) descriptive function names.
In a mathematical paper, often there's some notation that isn't defined and there isn't even any pointer where to look for definitions. Important objects are given one-letter names. Theorems are often only numbered; good luck remembering what lemma 2.17.3b was about. Proofs are written in prose (instead of something like Leslie Lamport proposed[0]). You have to fill in conceptual gaps and remind yourself of unstated assumptions. Notation and terminology is often ambiguous — what does "exponential time" mean? Is it DTIME(2^(c*n)) or DTIME(2^polynomial(n))? Does "increasing" mean "strictly increasing" or "non-decreasing"? Is zero a natural number? And so on.
A mathematical formalism that could be interpreted in a purely mechanical way would be a huge improvement.
[0] http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
- _dps 10y ago> Then how come an unfamiliar piece of source code is easier to follow than a mathematics paper using unfamiliar notation? This is clearly subjective. I read lots of mathematics research that I find more accessible than even pretty mundane source code (and yes, I write software for a living and have done so for over ten years).
- mcphage 10y agoThe answer to all of your questions: computer programs are written for computers to understand, and computers aren't very smart. Mathematical papers are written for mathematicians to understand, and they tend to be a lot smarter than computers.
- panic 10y agoMachine language is also written for computers to understand, but it's not easy to read. Computer-formalized math is usually even harder to read than regular notation. I don't think computers have much to do with this.
- mcphage 10y agoTrue, I should have said it better as, programming languages are written for compilers to read, and they're not very smart. Machine language is written for computers themselves. Computer-formalized math I don't think is written for anyone to read.
- wolfgke 10y ago> A mathematical formalism that could be interpreted in a purely mechanical way would be a huge improvement. Look at Homotopy Type Theory: > https://homotopytypetheory.org/ https://homotopytypetheory.org/
- Smaug123 10y agoI feel obliged to point out that HoTT is… really rather abstract. I'm just starting to learn about it now in my spare time, and I hold a master's degree in mathematics specialising in logic.
- Koshkin 10y agoIndeed, looks like scientific literature in general and mathematical literature in particular are stuck in the past century. As much as I enjoy reading printed materials, I often think that using a modern computer-based approach to presenting them could prove a lot superior. And no, PDF would not cut it, even with the possibility of hyperlinking. In my view, PDF is like the idea of the horseless carriage, or, rather, of a carriage pulled by a mechanical horse - a new technology stuck in the past. Looks like the modern web browser platform, on the other hand, could provide a reasonable base on which one could build an extremely powerful "IDE" for creating and interacting with mathematical expositions.