6 ms·

I'm of the mind that there is immense value in being able to figure out difficult proofs. Absolutely. However, the rabbit hole is very deep. Many papers make

I'm of the mind that there is immense value in being able to figure out difficult proofs. Absolutely. However, the rabbit hole is very deep. Many papers make leaps from one sentence to the next that, if you're not familiar with the field, can take a couple days to figure out. Even then, real world proofs are informal and therefore not air-tight. They're close enough, almost always, but there's a reason why a mathematical proof isn't considered valid unless it's lived for two years under peer scrutiny. One could drill down to formal proof in the Godelian sense, in which proofs are mere typography and can be checked mechanically, but that's not how most of real mathematics is done and, practically speaking, most of it can't be done that way and remain useful to humans (like assembly language, it's too low-level for most applications).

nnq 13y ago
> most of it can't be done that way and remain useful to humans (like assembly language, it's too low-level for most applications). Sincere question (I'm not a mathematician): why can't it be done that way?! On top of an assembly language you can create a higher level language and on top of that an even higher level one, and it is airtight, it has to be or the code won't compile or will throw a runtime exception, the compiler or interpreter doesn't just "roll a dice" when it comes across and ambiguous statement! You just can't have ambiguous statements, so starting from a "precise" assembler everything else built on top can absolutely be "air tight" at the language level. (Now concerning what the program actually ends up doing (like something else than you intended), or that sometimes you trade off security for speed and get a buffer overflow, ok, these things happen, but not at the language level! usually, and when they do - like C programs exploiting undefined but known for certain targets compiler behavior this is either advanced malicious obsfucation or random rookie mistakes.) So explaining the question: why can't one build a higher level mathematical language bottom up, starting from an "assembler" of machine-checkable proof steps and building one or a few levels of higher level human-friendly languages that still map unambiguously to the lower level one? Just because mathematical language has evolved in a top down fashion, starting with describing proofs in words or symbols derived from words, and then developing more an more precise language and systems, it doesn't mean that one can't go the reverse route, bottom up, an maybe meet closer to the top in a way, so that the resulting new mathematical language will be similar enough to classical one not to scare everyone away, right? ...and the benefits seem immense! Imagine: (1) replacing years of peer review replaced by machine checking basic correcting (+ some machine testing on huge data samples, for testable proofs, just to be sure there was no bug) (2) AI expert systems bringing real contributions to math by actually discovering new proofs AND providing them in a language understandable for humans, so humans learn from them and discover new techniques EDIT+: (3) allowing the development of much more advanced theories, because just as in software you can build much larger systems once you learn how to write more "bug free" code, the actual complexity of the proof could be much larger and maybe new realms of mathematical will become accessible to human understanding once we have a "linguistic aid" to reducing the percent of faulty proofs and the time spent debugging them
- nbouscal 13y ago
  I think it can in theory, but the reason it hasn't been done in practice is basically that mathematics is too damn big. Look at Whitehead and Russell's original attempt to do basically exactly what you're asking for: it took them a few hundred pages to build up enough machinery to prove that 1+1=2.
  - nnq 13y ago
    I never got to why this kind of work was stopped. I only heard the same argument (this is the phrasing from Wikipedia but everybody seems to say something along these lines): >"However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, there would in fact be some truths of mathematics which could not be deduced from them." ...so what?! The fact that there can be truths that can't be deduced from an "assembler language" just means that the system will sometimes just say something like "error: no proof in the current model database for 'fact x' found" and then the mathematician will just add "consider 'fact x' proven as in the defined in modelXYZ" (a model that can have a totally different logic than the current one - think of a model as a library written in a completely different programming language, in software analogy), taking responsibility for the fact the equivalence of the concepts 'fact x in current model' and 'fact x in modelXYZ'. The long term goal would be unification of as many of the models as possible (even with, what I understand from Godel, as the impossibility of total unification - if something is proved to be impossible, it doesn't mean you can't get great benefits by always getting asimptotically closer to it) preventing such "forced equivalences", but it would still be a working system in the meantime. And more importantly, I guess, the system will make the "forced equivalences" obvious, and label them as problems for mathematicians to solve.
    - DerpDerpDerp 13y ago
      Part of the problem is, how do you know you can't prove it rather than just that you haven't proved it, without some kinda of metatheory framework?
    - 13y ago

nnq 13y ago

> most of it can't be done that way and remain useful to humans (like assembly language, it's too low-level for most applications). Sincere question (I'm not a mathematician): why can't it be done that way?! On top of an assembly language you can create a higher level language and on top of that an even higher level one, and it is airtight, it has to be or the code won't compile or will throw a runtime exception, the compiler or interpreter doesn't just "roll a dice" when it comes across and ambiguous statement! You just can't have ambiguous statements, so starting from a "precise" assembler everything else built on top can absolutely be "air tight" at the language level. (Now concerning what the program actually ends up doing (like something else than you intended), or that sometimes you trade off security for speed and get a buffer overflow, ok, these things happen, but not at the language level! usually, and when they do - like C programs exploiting undefined but known for certain targets compiler behavior this is either advanced malicious obsfucation or random rookie mistakes.) So explaining the question: why can't one build a higher level mathematical language bottom up, starting from an "assembler" of machine-checkable proof steps and building one or a few levels of higher level human-friendly languages that still map unambiguously to the lower level one? Just because mathematical language has evolved in a top down fashion, starting with describing proofs in words or symbols derived from words, and then developing more an more precise language and systems, it doesn't mean that one can't go the reverse route, bottom up, an maybe meet closer to the top in a way, so that the resulting new mathematical language will be similar enough to classical one not to scare everyone away, right? ...and the benefits seem immense! Imagine: (1) replacing years of peer review replaced by machine checking basic correcting (+ some machine testing on huge data samples, for testable proofs, just to be sure there was no bug) (2) AI expert systems bringing real contributions to math by actually discovering new proofs AND providing them in a language understandable for humans, so humans learn from them and discover new techniques EDIT+: (3) allowing the development of much more advanced theories, because just as in software you can build much larger systems once you learn how to write more "bug free" code, the actual complexity of the proof could be much larger and maybe new realms of mathematical will become accessible to human understanding once we have a "linguistic aid" to reducing the percent of faulty proofs and the time spent debugging them

nbouscal 13y ago
I think it can in theory, but the reason it hasn't been done in practice is basically that mathematics is too damn big. Look at Whitehead and Russell's original attempt to do basically exactly what you're asking for: it took them a few hundred pages to build up enough machinery to prove that 1+1=2.
- nnq 13y ago
  I never got to why this kind of work was stopped. I only heard the same argument (this is the phrasing from Wikipedia but everybody seems to say something along these lines): >"However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, there would in fact be some truths of mathematics which could not be deduced from them." ...so what?! The fact that there can be truths that can't be deduced from an "assembler language" just means that the system will sometimes just say something like "error: no proof in the current model database for 'fact x' found" and then the mathematician will just add "consider 'fact x' proven as in the defined in modelXYZ" (a model that can have a totally different logic than the current one - think of a model as a library written in a completely different programming language, in software analogy), taking responsibility for the fact the equivalence of the concepts 'fact x in current model' and 'fact x in modelXYZ'. The long term goal would be unification of as many of the models as possible (even with, what I understand from Godel, as the impossibility of total unification - if something is proved to be impossible, it doesn't mean you can't get great benefits by always getting asimptotically closer to it) preventing such "forced equivalences", but it would still be a working system in the meantime. And more importantly, I guess, the system will make the "forced equivalences" obvious, and label them as problems for mathematicians to solve.
  - DerpDerpDerp 13y ago
    Part of the problem is, how do you know you can't prove it rather than just that you haven't proved it, without some kinda of metatheory framework?
  - 13y ago