https://lawrencecpaulson.github.io/2023/08/09/computer_proof.html

[utterances-bot]

When is a computer proof a proof?

https://lawrencecpaulson.github.io/2023/08/09/computer_proof.html

[phlegmaticprogrammer]

Michael Harris calls the third property (Proofs are formalisable) the "Central Dogma" (https://mathematicswithoutapologies.wordpress.com/2022/01/19/the-central-dogma-of-mathematical-formalism/). I agree with his position: Mathematics and proofs are not necessarily formal, and moreover, their correctness is not defined in terms of their formalisability (see for example the mutilated chessboard problem, which is easily understood without any knowledge of mathematics or formal logic). So I think it is important to emphasise, especially when constructing mathematical software, that informal mathematics and its correctness is not defined in terms of formal logic. Rather, it is a conjecture that all of correct informal mathematics can be faithfully represented in sound and consistent formal logic. I believe that conjecture to be true, and I think mathematical software should strive to be the practical proof of this. It is fine when mathematical software inspires new mathematics and foundations, but if that means that standard mathematics is difficult to do in it, then it is not good enough (yet).

[lawrencecpaulson]

Regarding the linked quote, I'm not sure that Harris even understands what the philosophy of formalism is. Gödel was emphatically a Platonist, not formalist, and yet he asserted in 1935 that "everything mathematical is formalisable". I'm certain that Avigad is no formalist either. The philosophy of formalism asserts that mathematics is essentially a game played with meaningless strings of symbols. Wittgenstein and Curry seemed to hold that view. I don't think that even Hilbert was a formalist in his heart.

The correct way to interpret "formalisable" is not necessarily reduction to a formal calculus (and certainly not to a fixed calculus), but the ability to explain abstractions such as infinitesimals, functions and sets in absolutely concrete terms. Around the start of the 19th century, even the concept of a real number was unclear.

The mutilated chessboard problem is not about real chess boards but about an abstraction that is absolutely precise, which is what makes it mathematical. You are right if you insist that the particular way we represent this abstraction is irrelevant to the problem itself.

More here: https://encyclopediaofmath.org/wiki/Arithmetization_of_analysis

[phlegmaticprogrammer]

Harris points in one of his posts to this paper: https://doi.org/10.1007/s11229-022-03812-w

I found it a very interesting read. While I would agree with everything you said above (except maybe what Harris does or does not understand), I think the main point is that informal mathematics can be precise, yet not formal. Formal mathematics is one particular form of precise mathematics, but certainly not the only one. For example, it does not really matter if the chessboard is a real one, or just an abstract one: you cannot cover it with dominoes either way. What is going on here is perfectly clear and precise, without needing to refer to anything more complicated than the idea of a chessboard.

It seems to me in the above you try to make the point that precise and formalisable are the same thing. I think that is exactly the Central Dogma.

[lawrencecpaulson]

I certainly agree that informal mathematics can be precise, yet not formal. I would go further and say that essentially no published mathematics is formal. But it is formalisable. This is the outcome of a program that began in the mid 19th century. That all mathematics is formalisable has been accepted for nearly a century, and we have half a century of people testing this claim by actually formalising ambitious results.

To say that the claim is "dogma" (i.e. an assertion not backed by evidence) is to brush off all that work. I would turn it back and ask for evidence of the contrary. Give us just one single example, one piece of mathematics that is not formalisable. You have looked at Conway's Partizan Games, an interesting case because this work was not trivial to formalise. But the task was not especially difficult.

[phlegmaticprogrammer]

I feel like you are asking me to come up with a counter example to a conjecture (correct mathematics = formalisable mathematics) that I believe, but have no proof for, although plenty of heuristic evidence is available. I think it is important to insist that this is a conjecture, and not a proven theorem or even just a definition. This is important not just for philosophical reasons, but especially for practical reasons: Why exactly is it that some informal proofs are clear and easy, but burdensome to formalise? Each time this is encountered, we need to drill into this, and try to get rid of the discrepancy, without being dogmatic about it.

We don't know if all of mathematics is formalisable. The only way to show this is to actually formalise all of mathematics in a satisfying and faithful way (what does satisfying and faithful mean here, is that formalisable?), and this clearly hasn't been done yet, not even close, even though the achievements of Isabelle and other systems like Lean are becoming more impressive by the year.

Yes, I have looked at Conway's Partizan Games, and I found a nice and easy way to formalise it in Isabelle, but it left me unsatisfied, because now this datatype of games existed outside the universe of sets and as such was not particularly useful and somewhat alien. Just not as handy as it would be in informal mathematics. You could say that Partizan Games have been formalised, but in a way, they haven't been, not really. The formalisation subtly changed what we are talking about. I've tried years later to remedy this by tinkering with the logic (https://link.springer.com/chapter/10.1007/978-3-319-20615-8_6), but wasn't successful then.

Two years ago I finally managed to solve this problem: The problem was types. Types are artificial barriers, and getting rid of them allows to move formal mathematics closer to informal mathematics. This work is astonishingly hard to publish, mainly because it runs up against another dogma: The dogma of types. If my work turns out to be correct (and I would like to see a formalised proof of this), and has the practical implications I think it has, types are finished, and just relegated to being a quirk of history. Now I think this is a big deal, but I seem to be the only one with this opinion. Your formalisation of ZF in Isabelle's intuitionistic higher-order meta logic contains basically the same kind of idea, but you got the wrong meta logic, just as HOLZF is not the right foundation as well, because in the end, both approaches rely on types at their very foundation.

So here is an example of why it is important to keep trying to prove "correct mathematics = formalisable mathematics", and not just taking it as a given.