https://lawrencecpaulson.github.io/2023/10/04/Ochigame.html

[utterances-bot]

The concept of proof within the context of machine mathematics

https://lawrencecpaulson.github.io/2023/10/04/Ochigame.html

[YawarRaza7349]

I think it's important to recognize that proofs are used for (at least) two different purposes:

• To ascertain that a statement is correct.
• To enlighten a reader about a particular instance of mathematical reasoning.

People sometimes complain that machine proofs are not satisfying for the second purpose, but we should remember that the first purpose is also an important goal in mathematics (at least the parts that are applied to real world problems). The usefulness of machine proofs shouldn't be dismissed just because they don't also serve the (still important!) purpose of appealing to human aesthetics.

[lawrencecpaulson]

But remember, without transparency even the first purpose is not achieved. The main aim of legibility is simply to let the reader check that the computer proof makes sense. By now, everybody surely knows that computer systems can go wrong.

[SKolodynski]

formalisers distinct from the mathematicians themselves and forming an underclass

I have seen this idea formulated by people who have never written any formalized proofs (although I don't see this in the Ochigame's preprint, maybe I am missing something). I think it comes from an analogy with hiring someone to type a manuscript, or later to typeset it in LaTeX. I earned money this way when I was a student. Of course the analogy is false - someone typesetting a manuscript of a mathematical paper does not need to be an expert in the subject, general knowledge of mathematical notation is sufficient. In contrast, at least with current technology, someone who formalizes a proof needs to know about it everything there is to know, often more than the original author. As for purposes of proofs it's a matter of personal taste and terminology but I consider the second purpose essential for something to be called a proof. A proof has to convey knowledge on why the theorem is true. If it does not then it's not a proof, such thing should be called a verification script. Verification scripts are useful of course, note that they not only "ascertain that a statement is correct" but also certify that the author of the verification script knows why the theorem is true.

[lawrencecpaulson]

I may be guilty of exaggerating Ochigame's suggestion: he never used the word underclass. But there's quite a discussion of academic hierarchies on page 11, where he indicated that engineers have a lower status than physicists at SLAC (Stanford Linear Accelerator Centre).

[SKolodynski]

However, I think this

there will be an increasing need for interpreting computer-generated proofs and explaining them to people

may indeed happen. Letting the imagination run, suppose someone evolves a population of NSLLM's (Not-So-Large Language Models) trained on a couple of million of resolved challenges generated from Metamath's set.mm, which ultimately produces a proof of the Riemann hypothesis, hundreds of thousands of lines long. Such proof could be a subject of research itself and mining useful information from such proofs may become a specialized knowledge area.