6 ms·

> Programming has existed for, say, 50-100 years. We have recorded mathematical history going back thousands, with contributions from most of the most brilliant

by xiaq 11y ago

> Programming has existed for, say, 50-100 years. We have recorded mathematical history going back thousands, with contributions from most of the most brilliant human beings to ever exist. Mathematics with a solid logic foundation has also existed only for the past century, and writing programs is actually equivalent to doing a mathematical proof as some have already pointed out. The actual problem is that when programming you are talking to computers, so you have to lay out each step, or the computer will not know what to do. Sure you can use libraries to do very complex things all at once, but then that's because those libraries have already laid out the steps. But when doing mathematics you are talking to humans and you often skip steps in a very liberal way. There is indeed a library of theorems that is written down, but there is also an unwritten library of "it trivially follows", which, if a mathematician is asked to actually write it down, might feel humiliated. When you think that there is something so trivial that computers must be able to do, you still have to find or invent a library for that. When you think there is something in mathematics so trivial that it must be true, you just need to convince your audience. One day all mathematical papers will come with a formal proof, but that day has not yet arrived.

xiaq 11y ago
To clarify the last sentence: I am not criticizing mathematicians for not doing formal proofs. Often mathematical publications are not final "products" but explorations into new methods. Requiring formal proofs on every publication, with the status quo of computer-assisted proving, will surely impeded the development of mathematics. What I am saying is that I hope one day with the development of computer-assisted proving, the chores involved in doing formal proofs will be reduced to such a degree that mathematicians are more inclined to do them than not.
Certhas 11y ago
> writing programs is actually equivalent to doing a mathematical proof Only in the sense that writing in brainfuck is equivalent to writing in Python...
- xiaq 11y ago
  True, but the point is that in principle you can write very detailed, fully formal proofs, in exactly the same manner programs are written. The rest of my comment then discusses why it is not written that way. Doing formal proofs manually is like writing turing machine instructions. Computer-assisted proving gives you higher level tools, but apparently it is still not powerful enough to be accepted in mainstream. And unlike programming where you get stuck if you haven't invented higher level languages, mathematicians have the widely accepted tool of "it trivially follows". Bourbaki might disagree, though.
  - true_religion 11y ago
    That's a very illuminating analogy. Users of high-level languages, typically do not think about what the compiler is doing, and if in fact they do not know the compiler action--often the only way to find out is by reading the compilers source code. This is akin to looking a math paper seeing "it trivially follows..." and your only recourse to find out why it so trivially follows is to get a mathematics degree.
    - xiaq 11y ago
      There is still a key difference. With programming the information is always there. If you don't understand a higher level language but do understand the language in which the compiler is implemented, you can always read the compiler. The "it trivially follows", the information is simply missing. Gaining a mathematics degree will often give you the intellectual power of finding the missing pieces yourself, but the only sure way is to ask the authors themselves.
      - EvanPlaice 11y ago
        At least in programming it's possible to step into a function and/or work at multiple levels of abstraction. Getting a math degree just to be able to fill in the gaps created where 'it trivially follows' is equivalent to being required to memorize the API for a framework because clearly defined documentation is hidden behind a paywall. so called 'intellectual power' has little to do with it. What you're describing is familiarity with navigating a minefield of poorly structured information and tapping a academia (ie at a very high cost of entry) for 'special access' to resources that bridge the gaps. Of software development suffered from the same informational constraints and lack of innovation, we'd still be playing pong.
wfo 11y ago
Mathematical papers will not come with a formal proof until formal proof systems "auto-prove" button is strong enough to do everything for them and it can come as an afterthought that takes 5 minutes. Formal proofs do nothing to help understand the mathematics, all they do is help to check for errors in logic -- have you ever read a formal proof? They are leagues more obtuse and difficult to understand than any piece of mathematics from any field. A program is technically truth-value equivalent to doing a proof, but the resulting document/piece of text are MILES apart. The proof is an explanation in plain language to others who understand the topic why something is true. The formal proof is a sequence of opaque inference rules that the computer promises is equivalent to a real proof. It's the difference between understanding a formula and plugging it into your calculator. The calculator is more likely to compute correctly, but it gives you no help when it comes to actually understanding mathematics. Mathematicians as a community completely reject the notion of using formal proofs (while sometimes begrudgingly accepting they may be useful to check our work) because they completely miss the point of what we are actually doing.

by xiaq 11y ago

xiaq 11y ago

To clarify the last sentence: I am not criticizing mathematicians for not doing formal proofs. Often mathematical publications are not final "products" but explorations into new methods. Requiring formal proofs on every publication, with the status quo of computer-assisted proving, will surely impeded the development of mathematics. What I am saying is that I hope one day with the development of computer-assisted proving, the chores involved in doing formal proofs will be reduced to such a degree that mathematicians are more inclined to do them than not.

Certhas 11y ago

> writing programs is actually equivalent to doing a mathematical proof Only in the sense that writing in brainfuck is equivalent to writing in Python...

xiaq 11y ago
True, but the point is that in principle you can write very detailed, fully formal proofs, in exactly the same manner programs are written. The rest of my comment then discusses why it is not written that way. Doing formal proofs manually is like writing turing machine instructions. Computer-assisted proving gives you higher level tools, but apparently it is still not powerful enough to be accepted in mainstream. And unlike programming where you get stuck if you haven't invented higher level languages, mathematicians have the widely accepted tool of "it trivially follows". Bourbaki might disagree, though.
- true_religion 11y ago
  That's a very illuminating analogy. Users of high-level languages, typically do not think about what the compiler is doing, and if in fact they do not know the compiler action--often the only way to find out is by reading the compilers source code. This is akin to looking a math paper seeing "it trivially follows..." and your only recourse to find out why it so trivially follows is to get a mathematics degree.
  - xiaq 11y ago
    There is still a key difference. With programming the information is always there. If you don't understand a higher level language but do understand the language in which the compiler is implemented, you can always read the compiler. The "it trivially follows", the information is simply missing. Gaining a mathematics degree will often give you the intellectual power of finding the missing pieces yourself, but the only sure way is to ask the authors themselves.
    - EvanPlaice 11y ago
      At least in programming it's possible to step into a function and/or work at multiple levels of abstraction. Getting a math degree just to be able to fill in the gaps created where 'it trivially follows' is equivalent to being required to memorize the API for a framework because clearly defined documentation is hidden behind a paywall. so called 'intellectual power' has little to do with it. What you're describing is familiarity with navigating a minefield of poorly structured information and tapping a academia (ie at a very high cost of entry) for 'special access' to resources that bridge the gaps. Of software development suffered from the same informational constraints and lack of innovation, we'd still be playing pong.

wfo 11y ago

Mathematical papers will not come with a formal proof until formal proof systems "auto-prove" button is strong enough to do everything for them and it can come as an afterthought that takes 5 minutes. Formal proofs do nothing to help understand the mathematics, all they do is help to check for errors in logic -- have you ever read a formal proof? They are leagues more obtuse and difficult to understand than any piece of mathematics from any field. A program is technically truth-value equivalent to doing a proof, but the resulting document/piece of text are MILES apart. The proof is an explanation in plain language to others who understand the topic why something is true. The formal proof is a sequence of opaque inference rules that the computer promises is equivalent to a real proof. It's the difference between understanding a formula and plugging it into your calculator. The calculator is more likely to compute correctly, but it gives you no help when it comes to actually understanding mathematics. Mathematicians as a community completely reject the notion of using formal proofs (while sometimes begrudgingly accepting they may be useful to check our work) because they completely miss the point of what we are actually doing.