Present day mathematics is a human construct, where computers are used more and more but do not play a creative role.
It always seemed very strange to me how, despite the obvious similarities and overlaps between mathematics and computer science, the use of computers for mathematics has largely been a fringe movement and mathematicians mostly still do mathematics the way it was done in the 19th century. This even though precision and accuracy is highly valued in mathematics and decades of experience in computer science has shown us just how prone humans are to making mistakes in programs, proofs, etc. and just how stubbornly these mistakes can evade the eyes of proof-checkers.
Correctness is essential, but another highly desirable property of a mathematical proof is its insightfulness, that is, whether they contain interesting and novel ideas that can later be reused in others’ work (often they are regarded as more important than a theorem itself). These others are humans and they desire, let’s call it, “human-style” insights. Perhaps if we had AIs that “desired” “computer-style” insights, some people (and AIs) would write their papers to provide them and investigate problems that are most likely to lead to them. Proofs that involve computers are often criticized for being uninsightful.
Proofs that involve steps that require use of computers (as opposed to formal proofs that employ proof assistants) are sometimes also criticized for not being human verifiable, because while both humans make mistakes and computer software can contain bugs, mathematicians sometimes can use their intuition and sanity checks to find the former, but not necessarily the latter.
Mathematical intuition is developed by working in an area for a long time and being exposed to various insights, heuristics, ideas (mentioned in a first paragraph). Thus not only computer based proofs are harder to verify, but also if an area relies on a lot of non human verifiable proofs that means it might be significantly harder to develop an intuition in that area which might then make it harder for humans to create new mathematical ideas. It is probably easier understand the landscape of ideas that were created to be human understandable.
That is neither to say that computers have little place in mathematics (they do, they can be used for formal proofs, generating conjectures or gathering evidence for what approach to use to solve a problem), nor it is to say that computers will never make human mathematicians obsolete (perhaps they will become so good that humans will no longer be able to compete).
However, it should be noted that some people have different opinions.
Automated theorem proving is a different problem entirely and it’s obviously not ready yet to take the place of human mathematicians. I’m not in disagreement with you here.
However there’s no conflict between being ‘insightful’ and ‘intuitive’ and being computer-verifiable. In the ideal case you would have a language for expressing mathematics that mapped well to human intuition. I can’t think of any reason this couldn’t be done. But that’s not even necessary—you could simply write human-understandable versions of your proofs along with machine-verifiable versions, both proving the same statements.
Substantial work has been done on this. The two major systems I know of are Automath (defunct but historically important) and Mizar (still alive). Looking at those articles just now also turns up Metamath. Also of historical interest is QED, which never really got started, but is apparently still inspiring enough that a 20-year anniversary workshop was held last year.
Creating a medium for formally verified proofs is a frequently occurring idea, but no-one has yet brought such a project to completion. These systems are still used only to demonstrate that it can be done, but they are not used to write up new theorems.
I thought there were several examples of theorems that had only been proved by computers, like the Four Color Theorem, but that they’re sort of in their own universe because they rely on checking thousands of cases, and so not only could a person not really be sure that they verified the proof (because the odds of them making a mistake would be so high) they couldn’t get much in the way of intuition or shared technique from the proof.
Indeed, the computer-generated proofs of 4CT were not only not formal proofs, they were not correct. Once a decade, someone would point out an error in the previous version and code his own. But now there is a version for an off the shelf verifier.
I think the difficulty is in part due to the fact that mathematicians use classical metalogic (e.g. proof by contradiction) which is not easily implemented in a computer system. The most famous mathematical assistant, Coq, is based on a constructive type theory. Even the univalence program, which is ambitious in its goal to formalize all mathematics, is based on a variant of intuitionistic meta-logic.
Converting most of existing math into formal developments suitable for computer use would be a huge undertaking, possibly requiring several hundred man-years of work. Most people aren’t going to work on such a goal with any seriousness until it’s clear to them that the results will in fact be widely used. This in turn requires further work in order to come up with lightweight, broadly-applicable logical foundations/frameworks, as well as more work on the usability of proof environments. Progress on these things has been quite slow, although we have seen some encouraging news lately, such as the recent ‘formal proof’ of the Kepler conjecture. And even that was actually a bunch of formal proofs developed under quite different systems, that can be argued to solve the conjecture only when they’re somehow combined. I think this example makes it abundantly clear that current approaches to this field—even at their most successful—do have non-trivial drawbacks.
You’re speaking of unifying all of math under the same system. I don’t think that’s strictly necessary, or even desirable. The computer science equivalent of that would be a development environment where every algorithm in the literature is implemented as a function.
I’m wondering more about why problem-specific computer-verifiable proofs aren’t used.
The problem is, no matter how ‘problem-specific’ your proofs are, they aren’t going to be ‘verifiable’ unless you specify them all the way down to some reasonable foundation. That’s the really big undertaking, so you’ll want to unify things as much as possible, if only to share whatever you can and avoid any duplication of effort.
The problem is, no matter how ‘problem-specific’ your proofs are, they aren’t going to be ‘verifiable’ unless you specify them all the way down to some reasonable foundation.
If that’s true then it logically follows that most existing mathematics literature is un-verifiable—a statement that I think mathematicians would take issue with. After all, that’s not how most mathematics literature is presented.
In the future, it would be best to derive everything from the axioms. (Using libraries where the frequently used theorems are already proved.) The problem is, the most simple theorems that we can derive from the axioms quickly are not important enough to pay for the development and use of the software.
So a better approach would be for the system to accept a few theorems as (temporary) axioms. Essentially, if it would be okay to use the Pythagorean theorem in a scientific paper without proving it, then in the first version of the program it would be okay to use the Pythagorean theorem as an axiom—displaying a warning “I have used Pythagorean theorem without having a proof of it”.
This first version would already be helpful at verifying current papers. And there is an option to provide the proof of the Pythagorean theorem from the first principles later. If you add it later, you can re-run the papers and get the results with less warnings. If the Pythagorean theorem happens to be wrong, as long as you have provided the warnings for all papers, you know which ones of them to retract.
Actually, I believe such systems would be super helpful e.g. in set theory, when you want to verify whether the proof you used does rely on the axiom of choice. Because even if you didn’t use it directly, maybe one of them theorems you used was based on it. Generally, using different sets of axioms could become easier.
Yes that’s an insightful way of looking at how computer verification could assist in real mathematics research.
Going back to the CS analogy, programmers started out by writing everything in machine language, then gradually people began to write commonly-used functions as libraries that you could just install and forget about (they didn’t even have to be in the same language) and they wrote higher-level languages that could automatically compile to machine code. Higher and higher levels of abstraction were recognized and implemented over the years (for implementing things like parsers, data structures, databases, etc.) until we got to modern languages like python and java where programming almost feels like simply writing out your thoughts. There was very little universal coordination in all of this; it just grew out of the needs of various people. No one in 1960 sat down and said, “Ok, let’s write python.”
until we got to modern languages like python and java where programming almost feels like simply writing out your thoughts. … No one in 1960 sat down and said, “Ok, let’s write python.”
For a very good reason: let me invite you to contemplate Python performance on 1960-class hardware.
As to “writing out your thoughts”, people did design such a language in 1959...
P.S. Oh, and do your thoughts flow like this..?
public class HelloWorld { public static void main(String[] args) { System.out.println("Hello World"); } }
For a very good reason: let me invite you to contemplate Python performance on 1960-class hardware.
That the implementation of python is fairly slow is a different matter, and high-level languages need not be any slower than, say, C or Fortran, as modern JIT languages demonstrate. It just takes a lot of work to make them fast.
As to “writing out your thoughts”, people did design such a language in 1959...
Lisp was also designed during that same period and probably proves your point even better. But 1960′s Lisp was as bare-bones as it was high-level; you still had to wrote almost everything yourself from scratch.
But 1960′s Lisp was as bare-bones as it was high-level; you still had to wrote almost everything yourself from scratch.
Computerized math is the same today. No one wants to write everything they need from scratch, unless they’re working in a genuinely self-contained (i.e. ‘synthetic’) subfield where the prereqs are inherently manageable. See programming languages (with their POPLmark challenge) and homotopy-type-theory as examples of such where computerization is indeed making quick progress.
Umm… LISP is elegant and expressive—you can (and people routinely do) construct complicated environments including DSLs on top of it. But that doesn’t make it high-level—it only makes it a good base for high-level things.
But if you use “high-level” to mean “abstracted away from the hardware” then yes, it was, but that doesn’t have much to do with “writing out your thoughts”.
For a very good reason: let me invite you to contemplate Python performance on 1960-class hardware.
LISP was definitely a thing in the 1960s, and python is not that different. For a long time, the former was pretty much ‘the one’ very-high-level, application-oriented language. Much like Python or Ruby today.
pretty much ‘the one’ … application-oriented language
Allow me to disagree again. LISP was lambda calculus made flesh and was very popular in academia. Outside of the ivory towers, the suits used COBOL, and the numbers people used Fortran (followed by a whole lot of Algol-family languages) to write their applications.
It always seemed very strange to me how, despite the obvious similarities and overlaps between mathematics and computer science, the use of computers for mathematics has largely been a fringe movement and mathematicians mostly still do mathematics the way it was done in the 19th century. This even though precision and accuracy is highly valued in mathematics and decades of experience in computer science has shown us just how prone humans are to making mistakes in programs, proofs, etc. and just how stubbornly these mistakes can evade the eyes of proof-checkers.
Correctness is essential, but another highly desirable property of a mathematical proof is its insightfulness, that is, whether they contain interesting and novel ideas that can later be reused in others’ work (often they are regarded as more important than a theorem itself). These others are humans and they desire, let’s call it, “human-style” insights. Perhaps if we had AIs that “desired” “computer-style” insights, some people (and AIs) would write their papers to provide them and investigate problems that are most likely to lead to them. Proofs that involve computers are often criticized for being uninsightful.
Proofs that involve steps that require use of computers (as opposed to formal proofs that employ proof assistants) are sometimes also criticized for not being human verifiable, because while both humans make mistakes and computer software can contain bugs, mathematicians sometimes can use their intuition and sanity checks to find the former, but not necessarily the latter.
Mathematical intuition is developed by working in an area for a long time and being exposed to various insights, heuristics, ideas (mentioned in a first paragraph). Thus not only computer based proofs are harder to verify, but also if an area relies on a lot of non human verifiable proofs that means it might be significantly harder to develop an intuition in that area which might then make it harder for humans to create new mathematical ideas. It is probably easier understand the landscape of ideas that were created to be human understandable.
That is neither to say that computers have little place in mathematics (they do, they can be used for formal proofs, generating conjectures or gathering evidence for what approach to use to solve a problem), nor it is to say that computers will never make human mathematicians obsolete (perhaps they will become so good that humans will no longer be able to compete).
However, it should be noted that some people have different opinions.
Automated theorem proving is a different problem entirely and it’s obviously not ready yet to take the place of human mathematicians. I’m not in disagreement with you here.
However there’s no conflict between being ‘insightful’ and ‘intuitive’ and being computer-verifiable. In the ideal case you would have a language for expressing mathematics that mapped well to human intuition. I can’t think of any reason this couldn’t be done. But that’s not even necessary—you could simply write human-understandable versions of your proofs along with machine-verifiable versions, both proving the same statements.
Substantial work has been done on this. The two major systems I know of are Automath (defunct but historically important) and Mizar (still alive). Looking at those articles just now also turns up Metamath. Also of historical interest is QED, which never really got started, but is apparently still inspiring enough that a 20-year anniversary workshop was held last year.
Creating a medium for formally verified proofs is a frequently occurring idea, but no-one has yet brought such a project to completion. These systems are still used only to demonstrate that it can be done, but they are not used to write up new theorems.
I thought there were several examples of theorems that had only been proved by computers, like the Four Color Theorem, but that they’re sort of in their own universe because they rely on checking thousands of cases, and so not only could a person not really be sure that they verified the proof (because the odds of them making a mistake would be so high) they couldn’t get much in the way of intuition or shared technique from the proof.
Yes, although as far as I know things like that, and the FCT in particular, have only been proved by custom software written for the problem.
There’s also a distinction between using a computer to find a proof, and using it to formalise a proof found by other means.
Indeed, the computer-generated proofs of 4CT were not only not formal proofs, they were not correct. Once a decade, someone would point out an error in the previous version and code his own. But now there is a version for an off the shelf verifier.
People are working on changing that (at CMU for example).
I think the difficulty is in part due to the fact that mathematicians use classical metalogic (e.g. proof by contradiction) which is not easily implemented in a computer system. The most famous mathematical assistant, Coq, is based on a constructive type theory. Even the univalence program, which is ambitious in its goal to formalize all mathematics, is based on a variant of intuitionistic meta-logic.
Converting most of existing math into formal developments suitable for computer use would be a huge undertaking, possibly requiring several hundred man-years of work. Most people aren’t going to work on such a goal with any seriousness until it’s clear to them that the results will in fact be widely used. This in turn requires further work in order to come up with lightweight, broadly-applicable logical foundations/frameworks, as well as more work on the usability of proof environments. Progress on these things has been quite slow, although we have seen some encouraging news lately, such as the recent ‘formal proof’ of the Kepler conjecture. And even that was actually a bunch of formal proofs developed under quite different systems, that can be argued to solve the conjecture only when they’re somehow combined. I think this example makes it abundantly clear that current approaches to this field—even at their most successful—do have non-trivial drawbacks.
You’re speaking of unifying all of math under the same system. I don’t think that’s strictly necessary, or even desirable. The computer science equivalent of that would be a development environment where every algorithm in the literature is implemented as a function.
I’m wondering more about why problem-specific computer-verifiable proofs aren’t used.
The problem is, no matter how ‘problem-specific’ your proofs are, they aren’t going to be ‘verifiable’ unless you specify them all the way down to some reasonable foundation. That’s the really big undertaking, so you’ll want to unify things as much as possible, if only to share whatever you can and avoid any duplication of effort.
If that’s true then it logically follows that most existing mathematics literature is un-verifiable—a statement that I think mathematicians would take issue with. After all, that’s not how most mathematics literature is presented.
I agree with that.
In the future, it would be best to derive everything from the axioms. (Using libraries where the frequently used theorems are already proved.) The problem is, the most simple theorems that we can derive from the axioms quickly are not important enough to pay for the development and use of the software.
So a better approach would be for the system to accept a few theorems as (temporary) axioms. Essentially, if it would be okay to use the Pythagorean theorem in a scientific paper without proving it, then in the first version of the program it would be okay to use the Pythagorean theorem as an axiom—displaying a warning “I have used Pythagorean theorem without having a proof of it”.
This first version would already be helpful at verifying current papers. And there is an option to provide the proof of the Pythagorean theorem from the first principles later. If you add it later, you can re-run the papers and get the results with less warnings. If the Pythagorean theorem happens to be wrong, as long as you have provided the warnings for all papers, you know which ones of them to retract.
Actually, I believe such systems would be super helpful e.g. in set theory, when you want to verify whether the proof you used does rely on the axiom of choice. Because even if you didn’t use it directly, maybe one of them theorems you used was based on it. Generally, using different sets of axioms could become easier.
Yes that’s an insightful way of looking at how computer verification could assist in real mathematics research.
Going back to the CS analogy, programmers started out by writing everything in machine language, then gradually people began to write commonly-used functions as libraries that you could just install and forget about (they didn’t even have to be in the same language) and they wrote higher-level languages that could automatically compile to machine code. Higher and higher levels of abstraction were recognized and implemented over the years (for implementing things like parsers, data structures, databases, etc.) until we got to modern languages like python and java where programming almost feels like simply writing out your thoughts. There was very little universal coordination in all of this; it just grew out of the needs of various people. No one in 1960 sat down and said, “Ok, let’s write python.”
For a very good reason: let me invite you to contemplate Python performance on 1960-class hardware.
As to “writing out your thoughts”, people did design such a language in 1959...
P.S. Oh, and do your thoughts flow like this..?
That the implementation of python is fairly slow is a different matter, and high-level languages need not be any slower than, say, C or Fortran, as modern JIT languages demonstrate. It just takes a lot of work to make them fast.
Lisp was also designed during that same period and probably proves your point even better. But 1960′s Lisp was as bare-bones as it was high-level; you still had to wrote almost everything yourself from scratch.
Computerized math is the same today. No one wants to write everything they need from scratch, unless they’re working in a genuinely self-contained (i.e. ‘synthetic’) subfield where the prereqs are inherently manageable. See programming languages (with their POPLmark challenge) and homotopy-type-theory as examples of such where computerization is indeed making quick progress.
Umm… LISP is elegant and expressive—you can (and people routinely do) construct complicated environments including DSLs on top of it. But that doesn’t make it high-level—it only makes it a good base for high-level things.
But if you use “high-level” to mean “abstracted away from the hardware” then yes, it was, but that doesn’t have much to do with “writing out your thoughts”.
LISP was definitely a thing in the 1960s, and python is not that different. For a long time, the former was pretty much ‘the one’ very-high-level, application-oriented language. Much like Python or Ruby today.
8-0 Allow me to disagree.
Allow me to disagree again. LISP was lambda calculus made flesh and was very popular in academia. Outside of the ivory towers, the suits used COBOL, and the numbers people used Fortran (followed by a whole lot of Algol-family languages) to write their applications.