Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: efji <efji@efi.efji>
Newsgroups: sci.math
Subject: Re: Log i = 0
Date: Sun, 25 May 2025 20:41:15 +0200
Organization: A noiseless patient Spider
Lines: 42
Message-ID: <100vo8d$1gvu4$1@dont-email.me>
References: <sYEiFg9bb-rpcOy6CMCFxOsQvKw@jntp> <100u1hr$164q1$1@dont-email.me>
 <h0z1WzuRt17jRInBMV41NIJRQYo@jntp> <100v4db$1clol$1@dont-email.me>
 <100vb6e$1e1uv$1@dont-email.me> <100ve7j$1ek0p$1@dont-email.me>
 <100vf19$1ela4$1@dont-email.me> <100vfr3$1ek0p$2@dont-email.me>
 <100vih5$1fh1n$1@dont-email.me> <100vjba$1fogg$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 25 May 2025 20:41:18 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="d96c330fc3cadd880eac3412a99394a5";
	logging-data="1605572"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+fR7glY5+fYOpk0p/E+35Q"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:wCsMQeueQK02ZdK5nnH0H4pA/zA=
In-Reply-To: <100vjba$1fogg$1@dont-email.me>
Content-Language: fr, en-US
Bytes: 3161

Le 25/05/2025 à 19:17, sobriquet a écrit :
> Humans are fallible creatures. Math communities consist of humans. 
> Conclusion, there is no certainty in math. Though of course it's 
> extremely unlikely for something to turn out to be false if its proof 
> has been verified and accepted by the entire community of mathematicians 
> and has stood the test of time. But there are also other factors 
> involved. For instance the proof could consist of terabytes of data, so 
> in that case we might increase our confidence level if we formalize the
> proof so it gets checked independently by a computer.

It seems that your level in mathematics may not be very advanced, and 
you appear to be repeating, somewhat awkwardly, what you’ve read in 
mainstream media.

No, proofs of theorems generally do not involve "terabytes of data" :)

ChatGPT gives the following rough evaluations:

* 3 to 5 millions of theorems proved since the beginning of humanity, 
some of them with multiple proofs (e.g. Pythagorean Theorem: more than 
400 independent proofs).

* 250000 to 350000 theorems published last year (between 100000 and 
120000 maths publications in peer reviews).

Among these millions of theorems, only a few involve a computer to help 
the proof. The first one was the "4 colors Theorem" in 1976 that used a 
computer to check 1936 identified configurations, too long to check 
manually.

Each year, a few theorems use computers to be proved, either using 
"proof assistants" that formalize and check the logic of hundreds of 
pages of inductions, or, like in the case of the 4 colors Theorem, check 
a finite number of remaining cases (possibly big) while the main human 
proof says something like "for n>N, blablabla".

But although the mainstream media talk a lot about them, they are 
totally marginal in the crowd of new theorems.


-- 
F.J.