What is a valid proof in algebra? It’s a proof where, in each step, we do something that is universally allowed, something which can only produce true equations from true equations, and so the proof gradually transforms the starting equation into a final equation which must be true if the starting equation was true. Each step should also—this is part of what makes proofs useful in reasoning—be locally verifiable as allowed, by looking at only a small number of previous points, not the entire past history of the proof.
Note that this doesn’t really solve the same problem that the quotes in the introduction are trying to solve. Proofs need to be valid and convincing. The ‘valid’ part is explained in the above. But the definition of the ‘convincing’ part is hidden in the phrase ‘locally verifiable’. It is not clear what locally verifiable means, so this simply leaves open that part of the definition.
Put differently, you could still define
locally verifiable:⟺the mathematicians who read it can correctly assess whether this step is valid
which is the social approach; or
locally verifiable:⟺ the mathematician who wrote it is capable of transforming the step into a sequence of steps that are valid according to a formal proof system
which is arguably the proper version of the symbolic approach. Both would fit with the explanation above.
(I’m not claiming that leaving this part open makes it a worthless definition, just that it can’t be fairly compared to the opening quotes, as those are, in fact, trying to define the convincing part. They’re attempts (not necessarily good ones) at solving a strictly harder problem.)
Note that this doesn’t really solve the same problem that the quotes in the introduction are trying to solve. Proofs need to be valid and convincing. The ‘valid’ part is explained in the above. But the definition of the ‘convincing’ part is hidden in the phrase ‘locally verifiable’. It is not clear what locally verifiable means, so this simply leaves open that part of the definition.
Put differently, you could still define
which is the social approach; or
which is arguably the proper version of the symbolic approach. Both would fit with the explanation above.
(I’m not claiming that leaving this part open makes it a worthless definition, just that it can’t be fairly compared to the opening quotes, as those are, in fact, trying to define the convincing part. They’re attempts (not necessarily good ones) at solving a strictly harder problem.)