Re: Is Intel exceptionally unsuccessful as an architecture designer?

On 07/10/2024 18:59, Stefan Monnier wrote:

kinds of proofs as "better" than others.  Some dislike "proof by computer",
and don't consider the four-colour theorem to be a proven theorem yet.

 "Proof by computer" can mean many different things.  The 1976 proof by
Appel&Haken failed to convince a number of mathematicians both because
of the use of a computer and because of the "inelegant", "brute
force" approach.
 Regarding the use of a computer, it relied on ad-hoc code which used
brute force to check some large number of subproblems.  For some
mathematicians, it was basically some opaque piece of code saying "yes",
with no reason to be confident that the code actually did what the
authors intended it to do.

Certainly for a "proof by computer" to be acceptable, the software involved needs to be considered part of the proof.  It needs to be something other mathematicians can read through and agree is correct, just like any other bit of the mathematical proof.  Some programming languages are more suitable for that task than others - typically you'll want something that can handle arbitrary precision integers, automatic garbage collection (so that the code is not cluttered with stuff that is irrelevant to the real task), and probably a functional programming language or style (which is more mathematical in outlook, and easier to prove).
And just like you want the "hand-written" maths to be checked by multiple mathematicians, computer-based proofs should be confirmed on different hardware (so your proof doesn't rely on the Pentium FDIV bug or similar), and ideally with the same algorithm re-implemented in more than one programming language.  The more redundancy you can get there, the more confidence you can have in the results.

 The 2005 proof by Gonthier also used a computer, but the program used
was a generic proof assistant.  Arguably some "opaque brute force" code
was used as well, but it generated actual evidence of its claims, which
was then mechanically checked by the proof assistant.
 That leaves a lot less room for arguing that it's not valid.
I haven't heard anyone express doubts about that proof yet.
           Stefan