11 ms·

Pure Maths in Crisis?

72 points by lelf 8y ago

F-0X 8y ago
I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect computation and software is certainly not a source of perfect logic.
- moomin 8y ago
  They’re not, but they’re spectacularly good at spotting dumb errors that humans are spectacularly bad at spotting. Me, I still haven’t got my head around how to prove something on a computer, but the principle is sound. Theoretically one could build the proof as some form of literate program.
  - chess93 8y ago
    A computer just does symbolic manipulation according to a list of rules (axioms) and the human/programmer specifies which sequence of symbolic manipulations to apply and then the computer simply states whether or not the specified manipulations transform the theorem in to the truth symbol. http://us.metamath.org/mpegif/mmcomplex.html http://us.metamath.org/mpegif/mmcomplex.html (Warning: I've never actually done much of this before so some details might be wrong.)
    - dwheeler 8y ago
      I have done some, thanks for pointing to that page! Here's a prettier version for most people (the "mpegif" version uses GIFs for math symbols, which works everywhere but doesn't look at nice): http://us.metamath.org/mpeuni/mmcomplex.html http://us.metamath.org/mpeuni/mmcomplex.html
- adamnemecek 8y ago
  You mean unlike human?
- dwheeler 8y ago
  > I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect computation and software is certainly not a source of perfect logic. The issue is not that computers are always perfect. The issue is that humans are far, far worse than computers at detecting errors in proofs. So-called proofs are later found to be wrong, even after lots of human peer review, and there are often doubts about published papers. If pure math is about proof (and it is), then checking proofs with only humans is unacceptable in the long term. Humans simply aren't good enough at it, and why should we make humans do a job (verifying proofs) when computers are obviously better at it? In addition, there are many mechanisms for countering computer errors that make their likelihood essentially zero. Hardware bugs happen, but executing software on multiple different computers using diverse CPUs basically makes that disappear. Software can have errors, but there are ways to counter that too. The Metamath community verifies set.mm (its main database at http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ) by running running 4 different verifiers that were implemented by four different developers in 4 different programming languages (C, Rust, Python, and Java). There are at least 13 different Metamath verifiers, so a few more could be added if desired. The underlying Metamath language is extremely simple, too, so a verifier can be written in only a few hundred lines of code (reducing the risk of error in any one of the verifiers). There's evidence that N-version programming doesn't reduce errors as quickly as if errors were independent (see Knight and Leveson's paper), but even so, it's still quite difficult to slip by that many independent verifiers. In the long term, proof verifiers can be proven correct. It's hard to prove large programs correct, but you only need to verify the verifier; there are already examples such as ivy for prover9. I can imagine that computers might someday be better at creating proofs. But that isn't necessary for computers to be useful. The main issue today is that proofs are typically not computer-verified, and computers can do that today. Many tools have managed to do well on Freek's "Formalizing 100 Theorems" challenge list at http://www.cs.ru.nl/%7Efreek/100/ http://www.cs.ru.nl/%7Efreek/100/ - and for the most part that is without a lot of investment. It's not easy to use existing tools, that's definitely true. But a big part of the problem is that there hasn't been a lot of work to use or grow them. If more work and money was invested in improving the systems for verifying proofs, and it was held in higher regard, a lot more would happen. I believe future mathematicians will view proofs unchecked by computers the same way we view alchemy today. I suspect they'll say something like, "once in a while those alchemists and pre-mathematicians happened to be correct, but of course we don't accept their work without computer verification today." I think we should be working to make that future happen sooner.
romwell 8y ago
Mathematics has always been like that. The Fundamental Theorem of Algebra went through many "proofs" over decades before settling on one we accept as rigorous. And rigor itself? A relatively modem requirement. Calculus was put on a rigorous basis only in the 19th century. It existed, and was applied, for centuries before that. The real truth about mathematics is that it's way more about intuition than rigor, and that things that most people think are true are taken as such. It's human nature, and mathematics is a human endeavor. Moreover, math itself resists rigor in a fundamental way, as Godel showed us. Machine proofs? Eh. Ultimately, everything is up to humans, even the axioms. Will the computer believe in the axiom of choice? And stuff that's too complex to be understood except for the select few? So be it. It means nobody really cares about that stuff. Maybe someone will discover a better proof later. Maybe someone will stumble upon a counterexample. Maybe nobody will touch that for a thousand years. Math will go on. Not that all math is accessible, but all good math is not limited to in-groups. For an extreme example, Grigori Perelman's famous work is surely not accessible, and is famously incomplete. It didn't matter. The ideas were clear to enough people around the world that it didn't take long for them to spread, and for others to step up and close the gaps. I've always said that mathematics is a form of art, perhaps with a smaller audience than most. The only criterion in mathematics is beauty: whether the work is interesting or not. Some works lack in that aspect, as it happens in all arts, and will not be appreciated by future generations. And it's fine. Disclaimer: I do math, sometimes.
- deleted 8y ago
  [deleted]
- dwheeler 8y ago
  > And rigor itself? A relatively modern requirement. Perhaps. I would argue that it is LONG overdue. > Moreover, math itself resists rigor in a fundamental way, as Godel showed us. This merely shows that some things cannot be proved, be it by machine or computer. That's not the issue. The issue is whether or not we should be moving towards machine-verified proofs, since "proofs" verified only by humans often turn out to be wrong. > Machine proofs? Eh. Ultimately, everything is up to humans, even the axioms. Will the computer believe in the axiom of choice? A computer will "believe" the axiom of choice if it is told that it is an axiom. I agree that the humans get to decide what is an axiom (at least in their system), but it should be immediately obvious exactly what axioms are being accepted, and then rigorously shown that only those accepted axioms are being used. I can even point to a demonstration. One of the mathematical formalization tools available today is Metamath ( http://us.metamath.org/ http://us.metamath.org/ ). In Metamath you can state the axioms you wish to accept, and then generate proofs that are automatically checked; every step must lead back to a previously-proved theorem or an axiom. There are several existing Metamath databases. The "set.mm" database (Metamath Proof Explorer) is based on classical logic, ZFC, and the axiom of choice. Since the axiom of choice is included as an axiom, you can use it. See here: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html In contrast, the "iset.mm" database (Intuitionistic Logic Explorer) is based on intuitionistic logic and does not include the axiom of choice. Since the axiom of choice is not included, you cannot verify a proof that tries to use it - the verifier will simply complain that the step is invalid if you try to do it. See here: http://us.metamath.org/ileuni/mmil.html http://us.metamath.org/ileuni/mmil.html
dannykwells 8y ago
I think articles like this are hilarious because they act like written down proofs are a gold standard of unassailable logic. Of course they aren't - what constitutes proof to one person (or in one age) may or may not constitute proof to others. Look at Mochizuki's work - someone so convinced they are right, and yet no one else can understand it: https://www.nature.com/news/the-biggest-mystery-in-mathematics-shinichi-mochizuki-and-the-impenetrable-proof-1.18509 https://www.nature.com/news/the-biggest-mystery-in-mathemati... Another good example: Euler's proofs in his day would be failed in even a basic real analysis class now. Having known many many pure mathematicians, I believe that they don't want to use computers for the simple reason that many of them don't know how to, and thus denying the legitimacy of computer-generated (or assisted) proofs protects their livelihood/careers.
- tacomonstrous 8y ago
  >denying the legitimacy of computer-generated proofs protects their livelihood/careers. While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. What is true is that there is still serious prejudice against theorems verified by reducing to a finite (yet large) number of concrete cases, which are then verified by an algorithm. This is the case even after the whole brouhaha over and resolution of the 4 colors theorem by Hales.
  - dannykwells 8y ago
    Good catch on the generated vs. assisted - I edited my comment.
  - auggierose 8y ago
    Hales didn't resolve the 4 colors theorem, Gonthier did that. Hales proved the Kepler Conjecture and afterwards facilitated its formal verification via the Flyspeck project.
    - wolfgke 8y ago
      > Hales didn't resolve the 4 colors theorem, Gonthier did that. Gonthier didn't resolve the 4 colors theorem, Appel and Haken did that. Gonthier just created the first computer-checked proof for the Four-color theorem.
klyrs 8y ago
As a computational mathematician... I should clarify; I write programs to construct and verify proofs in discrete mathematics, and also I'm a hacker obsessed with high performance code... I agree that mathematics is in crisis. Why? Because I'm an oddball rarity. My first supervisor was a hacker too, but my PhD supervisor thought I was a wizard. Professors, by and large, can't hack. Those who could, abandoned the field for CS. Students are rarely hackers - often the celebrated kids are groomed through Olympiad, then Putnam, and jump straight into grad school with nary a glance towards a computer -- until they are broken against the only language seen as practical: latex. Mathematics is innately about computation; every "proof" is an algorithm in disguise, and yet the field fails to attract talent because computation itself is treated with such disdain. Math has its own reproducibility crisis -- we don't write code that performs the tedious operations "left to the reader" and even when we do, journals won't post it. And I don't see a ton of progress. My old department has hired a few young professors since I graduated... none can hack. It's sad
- stabbles 8y ago
  I have no idea what you mean with hacking or hacker in this context
  - alex-wallish 8y ago
    program
  - 0815test 8y ago
    "Learn to code", perhaps.
    - lawrenceyan 8y ago
      Does anyone mind explaining what exactly this "Learn to code" saying is implying and where exactly it came from? At first glance, it seems pretty innocuous, but apparently a great deal of controversy has surrounded this statement recently. Is there some sort of hidden meaning I should be aware of here?
0815test 8y ago
There's not much that's new here - Freek Wedijk estimated the cost of formalizing the undergrad math curriculum in its entirety at 140 man-years, for a rough monetary cost well above the millions-of-dollars range - link @ https://www.cs.ru.nl/~freek/notes/index.html https://www.cs.ru.nl/~freek/notes/index.html Expensive to be sure, but not excessively so for a mostly one-time effort. Part of the problem though is that we are still far from having a reasonably-standard platform for formal math that could be expected to fully unlock its benefits. Most of the effort in formalization so far seems to be occurring in domains of "synthetic mathematics", which seem to be mostly self-contained and don't take much formalization effort to reach close to the research frontier.
- philipkglass 8y ago
  Billions of dollars? If it only takes 140 man-years that implies more than $14 million per man-year.
  - 0815test 8y ago
    Yup, I suppose that it's closer to the hundreds-of-millions range for the undergrad curriculum only, in a single system - maybe even a bit less than that. But that then leaves open the question of how to go the rest of the way to the actual research frontier in whatever domains of math you care about, plus the inherent uncertainty as to whether these efforts will in fact be useful, since these systems are in such an early state. You're right though that the way I phrased that was a bit confusing, so thanks!
fspeech 8y ago
For people not familiar with the subject (or Buzzard and his cohort) I recommend checking out the Zulip archive https://leanprover-community.github.io/archive/116395maths/index.html https://leanprover-community.github.io/archive/116395maths/i... Some of the (esp. earlier) threads are very illuminating on the process of constructing proofs using ITPs (interactive theorem provers). My personal experience is that modeling a suitable domain of math formally can be a very good pedagogical exercise. There are many fine points that are easy to ignore when doing math informally but a formal tool would not let you. This is particularly helpful when working on foundational subjects. When successful you are rewarded with the feeling of possessing the understanding at a level deeper than everyone else (most likely untrue, but certainly a typical expository paper or book could not cover the subject as thoroughly). That said note my use of the word "modeling". In a formalization attempt you may have in your head an isomorphism between the code and the mathematical objects under study but the isomorphism is not necessarily apparent or universally recognized. Beyond the most quotidian matters other people's modeling code (think of it as an API) may or may not fit with your conceptual models. Just like there are different programming languages and libraries, there is no universally accepted approach to encode mathematical constructs. Your claim of correctness is only as good as your axioms and definitions. Your theorem, with all definitions completely unfolded, will be an unreadable tangle of first order logic formulas that anyone would be hard pressed to recognize as universally meaningful -- though it is extremely likely to be logically sound. Even if no one questions the soundness of your logic there is no tool that can certify that your formal expression actually means what you say it means in a mathematical domain.
mcguire 8y ago
As an aside, "The Endoscopic Classification of Representations: Orthogonal and Symplectic Groups" is a damn good title. I'll assume it means something to someone, but all I can say is that I expect it to make a big hole in the ground.
mathgenius 8y ago
> Proof is the essence of mathematics. Proof may be essential, but it is not the essence of mathematics. Like many things, the essence of mathematics is beauty. In this mad world, of which academia is a part, we only seek to measure things. And how can you measure beauty? You cannot, or, at best, it is subjective. So, in place of beauty we have big complicated proofs, that no-one understands. John Conway, later on in life, decided to quit being a "real mathematician" and focus instead on trying to understand mathematics. His student Borcherds came up with a proof of Conway & Norton's moonshine conjecture, but Conway himself never accepted it. Why? Because it was too complicated, it couldn't possibly be the right explanation for moonshine. What a dude.

72 points by lelf 8y ago

F-0X 8y ago

I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect computation and software is certainly not a source of perfect logic.

moomin 8y ago
They’re not, but they’re spectacularly good at spotting dumb errors that humans are spectacularly bad at spotting. Me, I still haven’t got my head around how to prove something on a computer, but the principle is sound. Theoretically one could build the proof as some form of literate program.
- chess93 8y ago
  A computer just does symbolic manipulation according to a list of rules (axioms) and the human/programmer specifies which sequence of symbolic manipulations to apply and then the computer simply states whether or not the specified manipulations transform the theorem in to the truth symbol. http://us.metamath.org/mpegif/mmcomplex.html http://us.metamath.org/mpegif/mmcomplex.html (Warning: I've never actually done much of this before so some details might be wrong.)
  - dwheeler 8y ago
    I have done some, thanks for pointing to that page! Here's a prettier version for most people (the "mpegif" version uses GIFs for math symbols, which works everywhere but doesn't look at nice): http://us.metamath.org/mpeuni/mmcomplex.html http://us.metamath.org/mpeuni/mmcomplex.html
adamnemecek 8y ago
You mean unlike human?
dwheeler 8y ago
> I cannot understand this "solution" of turning to machine-verified proofs. Coq, Isabelle, etc. invariably contain bugs. Even if they didn't, you can still run into hardware bugs. Computers are not a source of perfect computation and software is certainly not a source of perfect logic. The issue is not that computers are always perfect. The issue is that humans are far, far worse than computers at detecting errors in proofs. So-called proofs are later found to be wrong, even after lots of human peer review, and there are often doubts about published papers. If pure math is about proof (and it is), then checking proofs with only humans is unacceptable in the long term. Humans simply aren't good enough at it, and why should we make humans do a job (verifying proofs) when computers are obviously better at it? In addition, there are many mechanisms for countering computer errors that make their likelihood essentially zero. Hardware bugs happen, but executing software on multiple different computers using diverse CPUs basically makes that disappear. Software can have errors, but there are ways to counter that too. The Metamath community verifies set.mm (its main database at http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ) by running running 4 different verifiers that were implemented by four different developers in 4 different programming languages (C, Rust, Python, and Java). There are at least 13 different Metamath verifiers, so a few more could be added if desired. The underlying Metamath language is extremely simple, too, so a verifier can be written in only a few hundred lines of code (reducing the risk of error in any one of the verifiers). There's evidence that N-version programming doesn't reduce errors as quickly as if errors were independent (see Knight and Leveson's paper), but even so, it's still quite difficult to slip by that many independent verifiers. In the long term, proof verifiers can be proven correct. It's hard to prove large programs correct, but you only need to verify the verifier; there are already examples such as ivy for prover9. I can imagine that computers might someday be better at creating proofs. But that isn't necessary for computers to be useful. The main issue today is that proofs are typically not computer-verified, and computers can do that today. Many tools have managed to do well on Freek's "Formalizing 100 Theorems" challenge list at http://www.cs.ru.nl/%7Efreek/100/ http://www.cs.ru.nl/%7Efreek/100/ - and for the most part that is without a lot of investment. It's not easy to use existing tools, that's definitely true. But a big part of the problem is that there hasn't been a lot of work to use or grow them. If more work and money was invested in improving the systems for verifying proofs, and it was held in higher regard, a lot more would happen. I believe future mathematicians will view proofs unchecked by computers the same way we view alchemy today. I suspect they'll say something like, "once in a while those alchemists and pre-mathematicians happened to be correct, but of course we don't accept their work without computer verification today." I think we should be working to make that future happen sooner.

romwell 8y ago

Mathematics has always been like that. The Fundamental Theorem of Algebra went through many "proofs" over decades before settling on one we accept as rigorous. And rigor itself? A relatively modem requirement. Calculus was put on a rigorous basis only in the 19th century. It existed, and was applied, for centuries before that. The real truth about mathematics is that it's way more about intuition than rigor, and that things that most people think are true are taken as such. It's human nature, and mathematics is a human endeavor. Moreover, math itself resists rigor in a fundamental way, as Godel showed us. Machine proofs? Eh. Ultimately, everything is up to humans, even the axioms. Will the computer believe in the axiom of choice? And stuff that's too complex to be understood except for the select few? So be it. It means nobody really cares about that stuff. Maybe someone will discover a better proof later. Maybe someone will stumble upon a counterexample. Maybe nobody will touch that for a thousand years. Math will go on. Not that all math is accessible, but all good math is not limited to in-groups. For an extreme example, Grigori Perelman's famous work is surely not accessible, and is famously incomplete. It didn't matter. The ideas were clear to enough people around the world that it didn't take long for them to spread, and for others to step up and close the gaps. I've always said that mathematics is a form of art, perhaps with a smaller audience than most. The only criterion in mathematics is beauty: whether the work is interesting or not. Some works lack in that aspect, as it happens in all arts, and will not be appreciated by future generations. And it's fine. Disclaimer: I do math, sometimes.

deleted 8y ago
[deleted]
dwheeler 8y ago
> And rigor itself? A relatively modern requirement. Perhaps. I would argue that it is LONG overdue. > Moreover, math itself resists rigor in a fundamental way, as Godel showed us. This merely shows that some things cannot be proved, be it by machine or computer. That's not the issue. The issue is whether or not we should be moving towards machine-verified proofs, since "proofs" verified only by humans often turn out to be wrong. > Machine proofs? Eh. Ultimately, everything is up to humans, even the axioms. Will the computer believe in the axiom of choice? A computer will "believe" the axiom of choice if it is told that it is an axiom. I agree that the humans get to decide what is an axiom (at least in their system), but it should be immediately obvious exactly what axioms are being accepted, and then rigorously shown that only those accepted axioms are being used. I can even point to a demonstration. One of the mathematical formalization tools available today is Metamath ( http://us.metamath.org/ http://us.metamath.org/ ). In Metamath you can state the axioms you wish to accept, and then generate proofs that are automatically checked; every step must lead back to a previously-proved theorem or an axiom. There are several existing Metamath databases. The "set.mm" database (Metamath Proof Explorer) is based on classical logic, ZFC, and the axiom of choice. Since the axiom of choice is included as an axiom, you can use it. See here: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html In contrast, the "iset.mm" database (Intuitionistic Logic Explorer) is based on intuitionistic logic and does not include the axiom of choice. Since the axiom of choice is not included, you cannot verify a proof that tries to use it - the verifier will simply complain that the step is invalid if you try to do it. See here: http://us.metamath.org/ileuni/mmil.html http://us.metamath.org/ileuni/mmil.html

dannykwells 8y ago

I think articles like this are hilarious because they act like written down proofs are a gold standard of unassailable logic. Of course they aren't - what constitutes proof to one person (or in one age) may or may not constitute proof to others. Look at Mochizuki's work - someone so convinced they are right, and yet no one else can understand it: https://www.nature.com/news/the-biggest-mystery-in-mathematics-shinichi-mochizuki-and-the-impenetrable-proof-1.18509 https://www.nature.com/news/the-biggest-mystery-in-mathemati... Another good example: Euler's proofs in his day would be failed in even a basic real analysis class now. Having known many many pure mathematicians, I believe that they don't want to use computers for the simple reason that many of them don't know how to, and thus denying the legitimacy of computer-generated (or assisted) proofs protects their livelihood/careers.

tacomonstrous 8y ago
>denying the legitimacy of computer-generated proofs protects their livelihood/careers. While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. What is true is that there is still serious prejudice against theorems verified by reducing to a finite (yet large) number of concrete cases, which are then verified by an algorithm. This is the case even after the whole brouhaha over and resolution of the 4 colors theorem by Hales.
- dannykwells 8y ago
  Good catch on the generated vs. assisted - I edited my comment.
- auggierose 8y ago
  Hales didn't resolve the 4 colors theorem, Gonthier did that. Hales proved the Kepler Conjecture and afterwards facilitated its formal verification via the Flyspeck project.
  - wolfgke 8y ago
    > Hales didn't resolve the 4 colors theorem, Gonthier did that. Gonthier didn't resolve the 4 colors theorem, Appel and Haken did that. Gonthier just created the first computer-checked proof for the Four-color theorem.

klyrs 8y ago

As a computational mathematician... I should clarify; I write programs to construct and verify proofs in discrete mathematics, and also I'm a hacker obsessed with high performance code... I agree that mathematics is in crisis. Why? Because I'm an oddball rarity. My first supervisor was a hacker too, but my PhD supervisor thought I was a wizard. Professors, by and large, can't hack. Those who could, abandoned the field for CS. Students are rarely hackers - often the celebrated kids are groomed through Olympiad, then Putnam, and jump straight into grad school with nary a glance towards a computer -- until they are broken against the only language seen as practical: latex. Mathematics is innately about computation; every "proof" is an algorithm in disguise, and yet the field fails to attract talent because computation itself is treated with such disdain. Math has its own reproducibility crisis -- we don't write code that performs the tedious operations "left to the reader" and even when we do, journals won't post it. And I don't see a ton of progress. My old department has hired a few young professors since I graduated... none can hack. It's sad

stabbles 8y ago
I have no idea what you mean with hacking or hacker in this context
- alex-wallish 8y ago
  program
- 0815test 8y ago
  "Learn to code", perhaps.
  - lawrenceyan 8y ago
    Does anyone mind explaining what exactly this "Learn to code" saying is implying and where exactly it came from? At first glance, it seems pretty innocuous, but apparently a great deal of controversy has surrounded this statement recently. Is there some sort of hidden meaning I should be aware of here?

0815test 8y ago

There's not much that's new here - Freek Wedijk estimated the cost of formalizing the undergrad math curriculum in its entirety at 140 man-years, for a rough monetary cost well above the millions-of-dollars range - link @ https://www.cs.ru.nl/~freek/notes/index.html https://www.cs.ru.nl/~freek/notes/index.html Expensive to be sure, but not excessively so for a mostly one-time effort. Part of the problem though is that we are still far from having a reasonably-standard platform for formal math that could be expected to fully unlock its benefits. Most of the effort in formalization so far seems to be occurring in domains of "synthetic mathematics", which seem to be mostly self-contained and don't take much formalization effort to reach close to the research frontier.

philipkglass 8y ago
Billions of dollars? If it only takes 140 man-years that implies more than $14 million per man-year.
- 0815test 8y ago
  Yup, I suppose that it's closer to the hundreds-of-millions range for the undergrad curriculum only, in a single system - maybe even a bit less than that. But that then leaves open the question of how to go the rest of the way to the actual research frontier in whatever domains of math you care about, plus the inherent uncertainty as to whether these efforts will in fact be useful, since these systems are in such an early state. You're right though that the way I phrased that was a bit confusing, so thanks!

fspeech 8y ago

For people not familiar with the subject (or Buzzard and his cohort) I recommend checking out the Zulip archive https://leanprover-community.github.io/archive/116395maths/index.html https://leanprover-community.github.io/archive/116395maths/i... Some of the (esp. earlier) threads are very illuminating on the process of constructing proofs using ITPs (interactive theorem provers). My personal experience is that modeling a suitable domain of math formally can be a very good pedagogical exercise. There are many fine points that are easy to ignore when doing math informally but a formal tool would not let you. This is particularly helpful when working on foundational subjects. When successful you are rewarded with the feeling of possessing the understanding at a level deeper than everyone else (most likely untrue, but certainly a typical expository paper or book could not cover the subject as thoroughly). That said note my use of the word "modeling". In a formalization attempt you may have in your head an isomorphism between the code and the mathematical objects under study but the isomorphism is not necessarily apparent or universally recognized. Beyond the most quotidian matters other people's modeling code (think of it as an API) may or may not fit with your conceptual models. Just like there are different programming languages and libraries, there is no universally accepted approach to encode mathematical constructs. Your claim of correctness is only as good as your axioms and definitions. Your theorem, with all definitions completely unfolded, will be an unreadable tangle of first order logic formulas that anyone would be hard pressed to recognize as universally meaningful -- though it is extremely likely to be logically sound. Even if no one questions the soundness of your logic there is no tool that can certify that your formal expression actually means what you say it means in a mathematical domain.

mcguire 8y ago

As an aside, "The Endoscopic Classification of Representations: Orthogonal and Symplectic Groups" is a damn good title. I'll assume it means something to someone, but all I can say is that I expect it to make a big hole in the ground.

mathgenius 8y ago

> Proof is the essence of mathematics. Proof may be essential, but it is not the essence of mathematics. Like many things, the essence of mathematics is beauty. In this mad world, of which academia is a part, we only seek to measure things. And how can you measure beauty? You cannot, or, at best, it is subjective. So, in place of beauty we have big complicated proofs, that no-one understands. John Conway, later on in life, decided to quit being a "real mathematician" and focus instead on trying to understand mathematics. His student Borcherds came up with a proof of Conway & Norton's moonshine conjecture, but Conway himself never accepted it. Why? Because it was too complicated, it couldn't possibly be the right explanation for moonshine. What a dude.