Path: ...!Xl.tags.giganews.com!local-4.nntp.ord.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Dec 2024 19:20:52 +0000
Subject: Re: Terence Tao, "Machine Assisted Proof"
Newsgroups: sci.math
References: <url12v$m5i4$2@solani.org>
 <YIadnaDB9KvAtEP4nZ2dnZfqnPudnZ2d@giganews.com>
From: Ross Finlayson <ross.a.finlayson@gmail.com>
Date: Thu, 26 Dec 2024 11:20:54 -0800
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101
 Thunderbird/38.6.0
MIME-Version: 1.0
In-Reply-To: <YIadnaDB9KvAtEP4nZ2dnZfqnPudnZ2d@giganews.com>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <XJ2cnWe2BdAJMfD6nZ2dnZfqnPadnZ2d@giganews.com>
Lines: 94
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-ybsB/ODK8b0VO7otnkZnmDycbBc9j//g856X6g8nQ2M2lqIzRb3AtxbjpXK1tI4F7lmCwQoanKgjsbU!aogBTLtBOzK70Mis4VZG3m6D/KD/28dsbpG3fo6I8pp7zyQccb6j15eFuAX1fkEQALSOQsQV31JB
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
Bytes: 4080

On 02/27/2024 10:26 AM, Ross Finlayson wrote:
> On 02/27/2024 08:02 AM, Mild Shock wrote:
>>
>> Terence Tao, "Machine Assisted Proof"
>> https://www.youtube.com/watch?v=AayZuuDDKP0
>
> So, "Lean is the new concept-script Begriff"?
>
> Mizar, Metamath, I suppose it was Mizar, and Z,
> that was going to "canonize a formal library
> of derivation methods and associated results".
>
> https://en.wikipedia.org/wiki/Mizar_system
>
> "Mizar: Since 1973...."
>
> Many type inference systems, ....
>
> "Classical" logic is "quasi-modal", ..., usually,
> "classical quasi-modal logic".
>
> https://en.wikipedia.org/wiki/Category:Large-scale_mathematical_formalization_projects
>
>
> https://en.wikipedia.org/wiki/Category:Formal_systems
>
> It seems like a reasonable sort of system,
> just, enumerates logical antinomies, then
> each of what results the principal branches
> of the singularities either way, makes little theories,
> with their limits and their incompleteness.
> An example of this is ZF as it's usually considered.
>
> The real issue for mathematics is getting to
> where the types, for completions, are in effect
> and actual, because, it's a real role for foundations.
>
> Or as he put it, "trusting the compiler".
>
>
> Isoperimetric theorems and packing problems,
> they're pretty related. Basically looking for
> when the angle of the packing and packed are
> same, given arbitrary configurations around, ....
>
>
> It seems like "New value of computer assistance?
> More like the entire field is already based on it."
>
> When they started pushing calculators in school,
> it was like, I'm going to need trig and 1/x and
> this fractional powers button is great, also e.
> The rest of the graphing was like "no, thanks,
> school already taught me".
>
> So, Kepler conjecture, sphere-packing, seems for
> a sort of equi-partitioning and equi-packing sort
> of approach, for the isoperimetric, the isopacked.
>
>
>
> Then he gets into Faltings purity and it's like
> the only reason we're talking about Faltings purity
> is because Scholze is dirty.
>
> "This theorem is essential...", euh, here this is
> the usual difference between "not.need T" and "need not.T",
>
>
> Homotopy Type Theory is the strength of ZFC plus
> two large cardinals, ..., it adds unvalency. Well, sure,
> it's not consistent anymore, but it is more complete.
>
> It's like a new math lib was announced, "you're right".
>
>
>
> Freiman-Rusza conjecture, looks interesting,
> it's in doubling-spaces.
>
>
> Old wrapped as new, ....
>
>
> I'm a fan, and kind of demand, Faltings purity.
>
>
> For cross-checking compilers is "a little language
> with a term re-write system that results Mizar, Metamath,
> Coq, Lean, lambda calculus, category theory, descriptive
> set theory, ....".
>
>