What's so hard about creating a piece of software with as minimal as possible mathematical axioms, defining a formal language in which one can create new constructs based on the existing ones, and then all research papers could be written in that language and its correctness verified by a computer?
$\begingroup$
$\endgroup$
2
-
2$\begingroup$ Nothing is "hard" about creating that software. In fact, such software exists. The "hard" part is pedantically writing down all proofs in said language. $\endgroup$– StevenCommented Jul 20, 2021 at 7:04
-
$\begingroup$ The first "hard" thing is to define mathematical objects that models actual proofs, and to define the behaviour/properties of these objects. The second "hard" thing is to formalise these mathematical objects so that they could be encoded in a symbolic way and so that their operations and properties could be used efficiently. $\endgroup$– AlexeyCommented Aug 18, 2021 at 10:23
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
Computer-Assisted Proof is a rather old field of research, and programs of that kind have already been made. Most of them relied on brute-force approaches, or graph search algorithms (BFS, DFS).
The thing is, first of all, it would not be trivial to define a language that can describe every possible problem (see: incompleteness theorems), and also, assuming you defined that language and found an optimal way to catch up with the current state of research, what would happen if you fed your magic algorithm a paper describing the correctness of the magic algorithm itself?
Edit: As mentioned by Steven, the obvious problem with this is that one would have to insert each and every proof by hand, so I assumed OP wanted to generate those proofs in a less "manual" way. Either way, the problem of defining such a language would still be a thing (an example of a failed attempt at that might be Russell's Principia).
-
3$\begingroup$ It seems to me that the question is not really about automated theorem proving but rather about automatically verifying (human-made) proofs written in a suitable formal language. $\endgroup$– StevenCommented Jul 20, 2021 at 9:49
-
$\begingroup$ You're right, but we humans don't usually start complex proofs from the axioms up, we rely on other results, and, as you mentioned in your other comment, most of the effort would be in writing all the proofs of theorems that have already been proven by humans, "extending the language". In order to use the program, one would have to "catch up with the current state of research" (and the only somewhat reasonable way would be by using CAP algorithms). Also, the problem of defining the language prescinds from what method is used to "catch up"... $\endgroup$ Commented Jul 20, 2021 at 10:05