Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Stefan Monnier <monnier@iro.umontreal.ca>
Newsgroups: comp.arch
Subject: Re: Is Intel exceptionally unsuccessful as an architecture designer?
Date: Mon, 07 Oct 2024 12:59:11 -0400
Organization: A noiseless patient Spider
Lines: 24
Message-ID: <jwvo73vc1e9.fsf-monnier+comp.arch@gnu.org>
References: <vcd3ds$3o6ae$2@dont-email.me> <86jzf4829c.fsf@linuxsc.com>
	<vcpojl$2ads5$1@dont-email.me> <vct3av$2tic0$17@dont-email.me>
	<vctb0s$32gol$1@dont-email.me> <vctbo2$32cko$3@dont-email.me>
	<vcv711$3b4hf$1@dont-email.me> <vcvji5$3co45$7@dont-email.me>
	<20240925104320.00007791@yahoo.com> <vdaakm$1facd$4@dont-email.me>
	<vdacqq$1jf40$1@dont-email.me> <vdd6tv$23gqs$1@dont-email.me>
	<vdd8d6$23nsh$1@dont-email.me>
	<ee430ac27c829d5514d5652aa2c6fad6@www.novabbs.org>
	<vdevtm$2c7jg$1@dont-email.me> <vdg6fs$2ko7g$1@dont-email.me>
	<vdh5q8$2pnkp$2@dont-email.me>
	<40853b34aae592d6cd8a19f017e3f7eb@www.novabbs.org>
	<lm2vj6Frf3oU1@mid.individual.net>
	<de251b3b38495a7d423015a83cc842cb@www.novabbs.org>
	<vdis8f$34tqa$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain
Injection-Date: Mon, 07 Oct 2024 18:59:17 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="e4af6d4fc32c30cab8f0367293c1992d";
	logging-data="1873544"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/fYJCjgjsGhADCe+zxZUcMmc9UiRUfltI="
User-Agent: Gnus/5.13 (Gnus v5.13)
Cancel-Lock: sha1:DfiU5b34d5ogxNTaKjDQyClBMDQ=
	sha1:nEQERitEIADx6zkN+3McGytbDM8=
Bytes: 2780

> 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.

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