3 ms·

I may be wrong here, but don't mathematicians sometimes "compute" in a meta-language that's sometimes more powerful, or less formal, than the system they are in

I may be wrong here, but don't mathematicians sometimes "compute" in a meta-language that's sometimes more powerful, or less formal, than the system they are inferring things about? Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next.

schoen 6y ago
> Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next. Nonetheless, we may still get to the second case because there are a couple of large projects that are trying to formalize all of mathematics in a way that a computer can verify. http://us.metamath.org/ http://us.metamath.org/ https://arxiv.org/abs/1910.09336 https://arxiv.org/abs/1910.09336 If these catch on and become a deeper part of the mathematics research process, mathematicians would still discuss "what's acceptable" in terms of their views of axioms, and they would presumably still discover proofs for theorems, but review for formal correctness of inferences could be an automatic process. Note that some pretty impressively complex and abstract theorems have successfully been formalized in these systems (and their proofs checked by machine), even starting from quite small axiom systems. Edit: In the mathlib paper they mention a much wider set of efforts along these lines: > In this section, we compare and contrast mathlib with other substantial formal libraries for mathematics, including libraries for Mizar [9,28], HOL Light [35], Isabelle/HOL [49], Coq/SSReflect [10,46], and Metamath [47]. Our goal here is not to provide detailed comparisons of the various de-sign choices, but, rather to sketch the design space in broad strokes, situate mathlib within it, and explain some of the decisions we have made. Our choice of comparisons is not meant to be exhaustive: there are also substantial mathematical libraries in HOL4 [55], ACL2 [42], PVS [50], and NuPRL [17], as well as notable libraries built on standard Coq, such as the Coquelicot analysis library [14].
redvenom 6y ago
There are two separate statements here: 1. Mathematicians often use relatively powerful systems, like reasoning in ZFC about Peano arithmetic. The consistency and completeness of axiomatic systems is what this article is about 2. Mathematicians pretty much exclusively use informal systems (compared to formal logic) for reasoning. The reason why that is is because it is just infeasible to reason typical mathematics using formal logic for most cases. However, it's important to realize that these two are orthogonal.

schoen 6y ago

> Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next. Nonetheless, we may still get to the second case because there are a couple of large projects that are trying to formalize all of mathematics in a way that a computer can verify. http://us.metamath.org/ http://us.metamath.org/ https://arxiv.org/abs/1910.09336 https://arxiv.org/abs/1910.09336 If these catch on and become a deeper part of the mathematics research process, mathematicians would still discuss "what's acceptable" in terms of their views of axioms, and they would presumably still discover proofs for theorems, but review for formal correctness of inferences could be an automatic process. Note that some pretty impressively complex and abstract theorems have successfully been formalized in these systems (and their proofs checked by machine), even starting from quite small axiom systems. Edit: In the mathlib paper they mention a much wider set of efforts along these lines: > In this section, we compare and contrast mathlib with other substantial formal libraries for mathematics, including libraries for Mizar [9,28], HOL Light [35], Isabelle/HOL [49], Coq/SSReflect [10,46], and Metamath [47]. Our goal here is not to provide detailed comparisons of the various de-sign choices, but, rather to sketch the design space in broad strokes, situate mathlib within it, and explain some of the decisions we have made. Our choice of comparisons is not meant to be exhaustive: there are also substantial mathematical libraries in HOL4 [55], ACL2 [42], PVS [50], and NuPRL [17], as well as notable libraries built on standard Coq, such as the Coquelicot analysis library [14].

redvenom 6y ago

There are two separate statements here: 1. Mathematicians often use relatively powerful systems, like reasoning in ZFC about Peano arithmetic. The consistency and completeness of axiomatic systems is what this article is about 2. Mathematicians pretty much exclusively use informal systems (compared to formal logic) for reasoning. The reason why that is is because it is just infeasible to reason typical mathematics using formal logic for most cases. However, it's important to realize that these two are orthogonal.