It is fascinating to read your opinion on this topic (although I admit to skipping some parts of your posts, as they are sometimes too intellectual for me; of course, I do this at my own peril). It is particularly interesting because I've met many of the actors in your posts. Clearly you feel that the computer will play an important role in the mathematics of the future, otherwise there would be no need for this blog. It took a while for me to understand what you mean by "central dogma", but after trying to explain it to a friend I think I understand now what you mean: The central dogma says that informal mathematics is deemed correct if and only if it corresponds to a valid formalization of it. Now, taken as a theorem, the central dogma might actually be true (and I believe it is). But of course, as a definition of the correctness of informal mathematics, it is not satisfactory, and as you pointed out, what does correspondence mean in the first place? I explained the mutilated chessboard problem to my girl-friend, and she understood why it is impossible to tile the mutilated board with dominoes. Without her knowing anything about mathematics or formal logic. So clearly, this is not a game, and it is real.
I believe I am currently the person in the world who understands the nature of logic best (I might be wrong about that though; my work hasn't been successfully peer-reviewed yet). It can be understood in terms of there being: 1) a mathematical universe; 2) operations on this mathematical universe; and 3) operators, which are just functionals on this mathematical universe, and provide a way for talking about operations. Truth is modelled as a value 𝖳 in the mathematical universe. All the fancy type theories you see in interactive theorem provers out there are just confusing complications of this simple model (saying stuff like this gets my papers rejected). Logic is really just a precise way of writing down your thoughts, and there is nothing mysterious about it, but in doing so, it is like making a deal with the devil: there can be many ways in which the precise contract can be fulfilled, not only the way you might think of.
My goal is to provide people with a software that is a "bicycle for their mathematical mind". Clearly something better than paper must be possible, and I believe formal logic is essential to it; as long as it doesn't feel like something to fight against beyond the intrinsic difficulty of the problem. Paper / LaTeX allows me to write down anything I want to, and logic must do the same. The advantage of software-enabled logic over paper is that logic actually "understands" what I am writing down, in the same way the devil would.
I feel you would actually be in favour of such a software that supports your thinking instead of pressing it onto preformed rails, although your blog seems to be directed against ITP (I think you claim neutrality or indifference somewhere, but if that is so, why write this blog). Am I wrong?
Regarding the digression on "collapsing the human agency":
Insofar as the eventual arrival of meta-maticians is concerned (and I was careful in going no further than "submitting a competitive paper", which is a natural next step after "working through all of the exercises in the Springer-Verlag Graduate Texts in Mathematics series"; "competitive doctoral thesis" is another way of putting it), my view is that "For us, there is only the trying. The rest is not our business." Where we (human mathematicians) do have agency is in making sense of the imminent encounter and reacting accordingly.
It is fascinating to read your opinion on this topic (although I admit to skipping some parts of your posts, as they are sometimes too intellectual for me; of course, I do this at my own peril). It is particularly interesting because I've met many of the actors in your posts. Clearly you feel that the computer will play an important role in the mathematics of the future, otherwise there would be no need for this blog. It took a while for me to understand what you mean by "central dogma", but after trying to explain it to a friend I think I understand now what you mean: The central dogma says that informal mathematics is deemed correct if and only if it corresponds to a valid formalization of it. Now, taken as a theorem, the central dogma might actually be true (and I believe it is). But of course, as a definition of the correctness of informal mathematics, it is not satisfactory, and as you pointed out, what does correspondence mean in the first place? I explained the mutilated chessboard problem to my girl-friend, and she understood why it is impossible to tile the mutilated board with dominoes. Without her knowing anything about mathematics or formal logic. So clearly, this is not a game, and it is real.
I believe I am currently the person in the world who understands the nature of logic best (I might be wrong about that though; my work hasn't been successfully peer-reviewed yet). It can be understood in terms of there being: 1) a mathematical universe; 2) operations on this mathematical universe; and 3) operators, which are just functionals on this mathematical universe, and provide a way for talking about operations. Truth is modelled as a value 𝖳 in the mathematical universe. All the fancy type theories you see in interactive theorem provers out there are just confusing complications of this simple model (saying stuff like this gets my papers rejected). Logic is really just a precise way of writing down your thoughts, and there is nothing mysterious about it, but in doing so, it is like making a deal with the devil: there can be many ways in which the precise contract can be fulfilled, not only the way you might think of.
My goal is to provide people with a software that is a "bicycle for their mathematical mind". Clearly something better than paper must be possible, and I believe formal logic is essential to it; as long as it doesn't feel like something to fight against beyond the intrinsic difficulty of the problem. Paper / LaTeX allows me to write down anything I want to, and logic must do the same. The advantage of software-enabled logic over paper is that logic actually "understands" what I am writing down, in the same way the devil would.
I feel you would actually be in favour of such a software that supports your thinking instead of pressing it onto preformed rails, although your blog seems to be directed against ITP (I think you claim neutrality or indifference somewhere, but if that is so, why write this blog). Am I wrong?
Regarding the digression on "collapsing the human agency":
Insofar as the eventual arrival of meta-maticians is concerned (and I was careful in going no further than "submitting a competitive paper", which is a natural next step after "working through all of the exercises in the Springer-Verlag Graduate Texts in Mathematics series"; "competitive doctoral thesis" is another way of putting it), my view is that "For us, there is only the trying. The rest is not our business." Where we (human mathematicians) do have agency is in making sense of the imminent encounter and reacting accordingly.