7 ms·

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what

Math is the most formal science there is. Why don't serious math journals require programmatically checked proofs for all publications, and instead rely on what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? P.S. Reviews are still needed to check novelty etc.

HenryKissinger 5y ago
> Math is the most formal science there is. Can you prove that?
- robbedpeter 5y ago
  Formality is technically the degree of mathiness applied to a domain, since formal logic and any other framework of formalization decomposes to mathematics. So... it's a tautology. Math is the most mathy math. Biology or psychology are less mathy maths. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... Having provablility holes in the formal system doesn't imply the existence of other systems that could be decomposed from currently known or unknown symbols. In this universe, information at the level of string theory seems to describe the limits, so math, as she is wrote, is as formal as it gets. The map is not the territory, so math, as a map, will always be less "formal" than reality itself. It's pretty firmly in second place, though.
  - ttctciyf 5y ago
    But if you only have maps and no territory, can you still be said to be doing cartography? :)
nerdponx 5y ago
Is it possible to even check such a proof programmatically? Do we have that kind of technology? Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?
- lostmsu 5y ago
  > Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper? The point of the checked proof is that your final theorem is almost definitely correct (you did not make mistakes in your deductions, unless the proof checker has a serious bug) if you can convince computer it derives from your axioms. You can convince humans without your proof being correct thought, because they might not spot an error.
- broken_symlink 5y ago
  There is a language called lean which is popular among mathematicians. Here is an article: https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ https://www.quantamagazine.org/building-the-mathematical-lib... A more recent article as well: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm...
  - nerdponx 5y ago
    My question was specifically referring to these huge 500 proofs that only a handful of people have even attempted to understand. What is the upper limit of what our current state-of-the-art proof assistants can handle?
    - lostmsu 5y ago
      The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.
jhgb 5y ago
> Math is the most formal science there is. That's assuming you ascribe to viewing math as science. > Why don't serious math journals require programmatically checked proofs for all publications Presumably it has something to do with why formalized mathematics is rare: it's hard. Even relatively simple concepts become quite hard to deal with when fully formalized. I suspect that mathematics on this level is simply not amenable to the treatment that you envision (at least today).
jacobolus 5y ago
> Why don't serious math journals require programmatically checked proofs ... Because that would take 2+ orders of magnitude more work, and nobody has the time/attention budget for it. This is sort of like asking: why did you single person write this 10-page short story instead of making a Hollywood-style feature film?
- lostmsu 5y ago
  Would it though? Are proof checkers much more complicated than LaTeX? If mathematicians are in certain ways similar to developers, I'd expect them to hate fighting with the layout of their papers, and love fighting with a proof checker for the formulas.
  - klyrs 5y ago
    > Are proof checkers much more complicated than LaTeX? In terms of lines of code, no. In terms of the learning curve, yes -- latex does a very good job of getting out of the way and letting a mathematician just write in English, where proof assistants require rigid structure that doesn't remotely resemble how (most) mathematicians think. In terms of runtime, oh my god, get out of town.
    - lostmsu 5y ago
      > In terms of runtime, oh my god, get out of town. I think you're mixing two different things here. Runtime is large for proof assistants, e.g. programs that can actually generate pieces of proof for you. Specifically the generation part. Verification of a complete proof were all the steps are provided like you would do in a paper should not, AFAIU, take a long time.
      - klyrs 5y ago
        Fair point. I'm coming from the perspective that mathematicians don't like to fill in pesky details that experts in their respective fields can figure out in an hour or ten.
      - 5y ago
qsort 5y ago
For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve. Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.
- lostmsu 5y ago
  There are multiple ways in which Google Mail while behaving incorrectly still be usable. But a theorem is not only useless if it is incorrect, it is dangerous.
turminal 5y ago
Because programmatically checked proofs don't work the way you think they do. And even programatically checked proofs are still programs. And programs still need code review.
- lostmsu 5y ago
  I understand that you might need a code review for the proof to look nice, but the point of a checked proof is that you don't need a separate code review for correctness. If it checks (sans internal checker issues) - it is correct.
  - deadbeef57 5y ago
    You still need to check that the definitions are correct. If you define `x^n = 42`, then proving FLT for `n > 2` is really easy. And proof checkers cannot check that you get the definitions right.
    - lostmsu 5y ago
      Thanks for pointing that out. This is still magnitudes less things to manually check for correctness than an entire proof.
eigenket 5y ago
Getting a proof, even in one that is amenable to computer verification into a form where you can actually verify it is a monumental task, like it can easily take multiple experts multiple years. Adding to this problem the intersection of mathematicians who understand computer aided verification and who understand a particular piece of research mathematics is often empty, and even if there are a handful of people who could do the necessary work they're often busy doing more interesting stuff. Finally I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. I think its unlikely that this will happen for a long time, for the simple reason that to feed a proof into a computer requires someone to dissect the proof to its logical bare bones in the first place, and the person doing the dissection is likely to notice any errors before they get round to feeding the problem into the computer.
- ouid 5y ago
  > I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. Right, because that's not how it works. Errors aren't discovered after the proof has been translated into machine language because that is the only step of the verification. As soon as the code is written, the proof is verified. Necessarily, then, any error discovery has to happen before that.
roywiggins 5y ago
> Why don't serious math journals require programmatically checked proofs for all publications Because mathematics has more or less worked fine for decades without it, and most mathematicians aren't programmers and aren't interested in it. Proofs are for understanding, not for technical correctness (though obviously the latter is very important). A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe (and, crucially, that their peers also already believe) into a computer system. That's not to say proof checkers aren't interesting in their own right, but there's lots of really quite good reasons why mathematics goes without them almost all of the time. Formal methods bring a lot to computing, where our programs fall apart constantly, but mathematical proofs almost always don't fall apart. And in computing, almost all programs don't have formal proofs of correctness! If any area needs them, it's in computing, not mathematics. You might as well ask why every compiler doesn't come with a proof of correctness: because it's already hard enough to build a compiler, let alone the monstrosity that would be a formal proof. The added benefit to a computer-checked proof is usually small to nil, and it's a ton of work. Like, way more work than just writing the proof.
- webmaven 5y ago
  > A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe into a computer system. I guess the question is which of "convincing a human" or "convincing a computer" is considered the higher bar. In any case, uncovering "what you believe that isn't so" is pretty important.
  - roywiggins 5y ago
    Right, but the ordinary methods of doing mathematics seem to be so good that the vast effort required to encode proofs well enough for a computer to check vastly dwarfs the benefit, at least for now. There's obviously been a lot of work done on proof assistants and maybe it will become easy and natural to formulate most proofs in a way a computer can check, but it's not anywhere close to that yet. The book explicating the proof discussed in the article is already 500 pages long, translating that into something a computer could check just isn't at all feasible yet.
klyrs 5y ago
> ...what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? I kinda feel like this question answers itself. On the other hand, I can't imagine this quagmire lasting another century, but the machine-assisted proof ecosystem hasn't reached adolescence yet.
andyjohnson0 5y ago
(Meta but I don't think the parent comment deserved to be downvoted. Maybe it's arguably wrong but it prompted replies that increased my understanding of the practice of maths.)
- lostmsu 5y ago
  Thanks for this remark. It is amusing to see this behavior, considering the comment is a question, to which responses seem to favor answer "no". The only part of the comment, that is actually a statement about peer review in mathematics being as bad or even worse in terms of assessing correctness, than reviewing large code changes. And nobody argues against that.
CamperBob2 5y ago
The slides that mahogany linked to [1] may give you some insight into this question. They're pretty interesting. [1] https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio...
joppy 5y ago
There are some huge (not insurmountable) obstacles to this happening. The biggest one, as I see it, is that so many mathematical objects need to be formalised into the system so that a theorem can even be stated, let alone its proof checked. Coming up with useful (and correct) formalisms of these objects, objects that mathematicians use constantly every day, are entire research projects of their own. There are some excellent talks by Kevin Buzzard about this, and where he sees it going in the future from a mathematician’s perspective. We’re getting there but progress is slow, and a large part of why it’s slow is that modern mathematics is fantastically complicated.

HenryKissinger 5y ago

> Math is the most formal science there is. Can you prove that?

robbedpeter 5y ago
Formality is technically the degree of mathiness applied to a domain, since formal logic and any other framework of formalization decomposes to mathematics. So... it's a tautology. Math is the most mathy math. Biology or psychology are less mathy maths. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... Having provablility holes in the formal system doesn't imply the existence of other systems that could be decomposed from currently known or unknown symbols. In this universe, information at the level of string theory seems to describe the limits, so math, as she is wrote, is as formal as it gets. The map is not the territory, so math, as a map, will always be less "formal" than reality itself. It's pretty firmly in second place, though.
- ttctciyf 5y ago
  But if you only have maps and no territory, can you still be said to be doing cartography? :)

nerdponx 5y ago

Is it possible to even check such a proof programmatically? Do we have that kind of technology? Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper?

lostmsu 5y ago
> Do you also have to review the proof checking code to make sure you didn't make any errors in transcription from the original paper? The point of the checked proof is that your final theorem is almost definitely correct (you did not make mistakes in your deductions, unless the proof checker has a serious bug) if you can convince computer it derives from your axioms. You can convince humans without your proof being correct thought, because they might not spot an error.
broken_symlink 5y ago
There is a language called lean which is popular among mathematicians. Here is an article: https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ https://www.quantamagazine.org/building-the-mathematical-lib... A more recent article as well: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm...
- nerdponx 5y ago
  My question was specifically referring to these huge 500 proofs that only a handful of people have even attempted to understand. What is the upper limit of what our current state-of-the-art proof assistants can handle?
  - lostmsu 5y ago
    The problem is not the limit of what proof checkers can handle - that probably goes beyond all known math. The problem is that long standing theories that 500 page proof is based on are not yet transcribed into formal language, so you'd need to do them first.

jhgb 5y ago

> Math is the most formal science there is. That's assuming you ascribe to viewing math as science. > Why don't serious math journals require programmatically checked proofs for all publications Presumably it has something to do with why formalized mathematics is rare: it's hard. Even relatively simple concepts become quite hard to deal with when fully formalized. I suspect that mathematics on this level is simply not amenable to the treatment that you envision (at least today).

jacobolus 5y ago

> Why don't serious math journals require programmatically checked proofs ... Because that would take 2+ orders of magnitude more work, and nobody has the time/attention budget for it. This is sort of like asking: why did you single person write this 10-page short story instead of making a Hollywood-style feature film?

lostmsu 5y ago
Would it though? Are proof checkers much more complicated than LaTeX? If mathematicians are in certain ways similar to developers, I'd expect them to hate fighting with the layout of their papers, and love fighting with a proof checker for the formulas.
- klyrs 5y ago
  > Are proof checkers much more complicated than LaTeX? In terms of lines of code, no. In terms of the learning curve, yes -- latex does a very good job of getting out of the way and letting a mathematician just write in English, where proof assistants require rigid structure that doesn't remotely resemble how (most) mathematicians think. In terms of runtime, oh my god, get out of town.
  - lostmsu 5y ago
    > In terms of runtime, oh my god, get out of town. I think you're mixing two different things here. Runtime is large for proof assistants, e.g. programs that can actually generate pieces of proof for you. Specifically the generation part. Verification of a complete proof were all the steps are provided like you would do in a paper should not, AFAIU, take a long time.
    - klyrs 5y ago
      Fair point. I'm coming from the perspective that mathematicians don't like to fill in pesky details that experts in their respective fields can figure out in an hour or ten.
    - 5y ago

qsort 5y ago

For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve. Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.

lostmsu 5y ago
There are multiple ways in which Google Mail while behaving incorrectly still be usable. But a theorem is not only useless if it is incorrect, it is dangerous.

turminal 5y ago

Because programmatically checked proofs don't work the way you think they do. And even programatically checked proofs are still programs. And programs still need code review.

lostmsu 5y ago
I understand that you might need a code review for the proof to look nice, but the point of a checked proof is that you don't need a separate code review for correctness. If it checks (sans internal checker issues) - it is correct.
- deadbeef57 5y ago
  You still need to check that the definitions are correct. If you define `x^n = 42`, then proving FLT for `n > 2` is really easy. And proof checkers cannot check that you get the definitions right.
  - lostmsu 5y ago
    Thanks for pointing that out. This is still magnitudes less things to manually check for correctness than an entire proof.

eigenket 5y ago

Getting a proof, even in one that is amenable to computer verification into a form where you can actually verify it is a monumental task, like it can easily take multiple experts multiple years. Adding to this problem the intersection of mathematicians who understand computer aided verification and who understand a particular piece of research mathematics is often empty, and even if there are a handful of people who could do the necessary work they're often busy doing more interesting stuff. Finally I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. I think its unlikely that this will happen for a long time, for the simple reason that to feed a proof into a computer requires someone to dissect the proof to its logical bare bones in the first place, and the person doing the dissection is likely to notice any errors before they get round to feeding the problem into the computer.

ouid 5y ago
> I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. Right, because that's not how it works. Errors aren't discovered after the proof has been translated into machine language because that is the only step of the verification. As soon as the code is written, the proof is verified. Necessarily, then, any error discovery has to happen before that.

roywiggins 5y ago

> Why don't serious math journals require programmatically checked proofs for all publications Because mathematics has more or less worked fine for decades without it, and most mathematicians aren't programmers and aren't interested in it. Proofs are for understanding, not for technical correctness (though obviously the latter is very important). A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe (and, crucially, that their peers also already believe) into a computer system. That's not to say proof checkers aren't interesting in their own right, but there's lots of really quite good reasons why mathematics goes without them almost all of the time. Formal methods bring a lot to computing, where our programs fall apart constantly, but mathematical proofs almost always don't fall apart. And in computing, almost all programs don't have formal proofs of correctness! If any area needs them, it's in computing, not mathematics. You might as well ask why every compiler doesn't come with a proof of correctness: because it's already hard enough to build a compiler, let alone the monstrosity that would be a formal proof. The added benefit to a computer-checked proof is usually small to nil, and it's a ton of work. Like, way more work than just writing the proof.

webmaven 5y ago
> A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe into a computer system. I guess the question is which of "convincing a human" or "convincing a computer" is considered the higher bar. In any case, uncovering "what you believe that isn't so" is pretty important.
- roywiggins 5y ago
  Right, but the ordinary methods of doing mathematics seem to be so good that the vast effort required to encode proofs well enough for a computer to check vastly dwarfs the benefit, at least for now. There's obviously been a lot of work done on proof assistants and maybe it will become easy and natural to formulate most proofs in a way a computer can check, but it's not anywhere close to that yet. The book explicating the proof discussed in the article is already 500 pages long, translating that into something a computer could check just isn't at all feasible yet.

klyrs 5y ago

> ...what essentially is a code review for a very large change request with extremely convoluted code to be vetted bug free by only a handful of experts? I kinda feel like this question answers itself. On the other hand, I can't imagine this quagmire lasting another century, but the machine-assisted proof ecosystem hasn't reached adolescence yet.

andyjohnson0 5y ago

(Meta but I don't think the parent comment deserved to be downvoted. Maybe it's arguably wrong but it prompted replies that increased my understanding of the practice of maths.)

lostmsu 5y ago
Thanks for this remark. It is amusing to see this behavior, considering the comment is a question, to which responses seem to favor answer "no". The only part of the comment, that is actually a statement about peer review in mathematics being as bad or even worse in terms of assessing correctness, than reviewing large code changes. And nobody argues against that.

CamperBob2 5y ago

The slides that mahogany linked to [1] may give you some insight into this question. They're pretty interesting. [1] https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio...

joppy 5y ago

There are some huge (not insurmountable) obstacles to this happening. The biggest one, as I see it, is that so many mathematical objects need to be formalised into the system so that a theorem can even be stated, let alone its proof checked. Coming up with useful (and correct) formalisms of these objects, objects that mathematicians use constantly every day, are entire research projects of their own. There are some excellent talks by Kevin Buzzard about this, and where he sees it going in the future from a mathematician’s perspective. We’re getting there but progress is slow, and a large part of why it’s slow is that modern mathematics is fantastically complicated.