> 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.
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].
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/
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].