You know, it's always kind of bothered me that we constantly run into these "it's far too soon to say whether the proof is correct" issues. They're proofs. It should be apparent whether they are correct. Otherwise, are they really proof? As a layman who's only familiar with Hilbert's work as it pertains to Godel and CS, I'm curious what makes expressing these proofs using some sort of formal logic so difficult.
In this particular case, the proof literally hasn’t been written up yet! The papers are works in progress, only one of which has been even posted as a preprint so far.
But in general it’s reasonably common for a proof to have been written up to the best of the author’s ability, and for it still to be impossible for anyone else to understand it well enough to be confident in its correctness.
Formal logic was no help, for two reasons. First of all the formal logical systems of the early 20th century were really a sort of existence proof, to show that a formal logical system can in principle be defined, and were too unwieldy and verbose for practical use in non-trivial situations. Secondly, it would then become necessary for the reader to check the correctness of a proof in formal logic, which is an even more difficult task than checking a well-written informal proof.
But this is changing: modern formal proof systems are designed with user-friendliness in mind, and produce proofs that can be verified by computer. It’s now starting to happen that formalisation can be used as a way out of the impasse where a proof is too complicated for anyone but the author to understand. I can think of two examples of this: Thomas Hales’s Flyspeck project [1] was the first such case, and required a monumental effort from Hales and his collaborators. Much more recently, Randall Holmes’s proof that NF is consistent was formalised [2], finally putting to rest a very old question in the foundations of logic.
Expressing proofs as formal logic is a great tool to make them more rigorous. Formal proofs are easier to check with a computer, provided that all the cases have been fleshed out, and that it has been written in a proof-assistant language. However those proofs are tedious to write, and a human reader has a limited capacity for handling high number of cases. Omitting cases and writing out informally why those cases can be omitted is crucial to help the reader to follow the proof. That is a step where errors can arise.
An example of wrong proof due to sketching quickly some cases is the proof that all triangles are isosceles [1].
Here is also an example of an apparently obvious result with a non-trivial proof, were all the cases are written out formally in the proof-assistant language Coq [2]. It is the proof that if we compute the multiplications and the square roots with floating-point arithmetic in base 2, then sqrt(a*a) is actually |a|. This was assumed without proof in some previous papers, and it is easy to understand how the authors may have missed it. Note that this result is not true in base 10.
Finally, sometimes non-formal proof can actually be more convincing than formal proof. For example, it was proven formally in 1957 that it is possible to turn a sphere inside out continuously, without cutting it, tearing it or creating any crease [3]. With more work, this result was later proven with a video. The video proof is arguably easier to follow and more convincing for a human. The formal proof has not yet been formally checked by a proof assistant, although work in this direction is on the way [4].
Proofs are literature. They need to go through a peer review process to have someone other than the author verify their correctness. Nowadays often tools like Lean are used to convert the argument into what you would call formal logic. It's nontrivial and takes time.
> As a layman who's only familiar with Hilbert's work as it pertains to Godel and CS, I'm curious what makes expressing these proofs using some sort of formal logic so difficult.
For one thing, they'd be much longer, and likely not human-readable.
