On the adoption of formalised math

[Sam Sanders]

Dear Harvey, 

The point of discussion is (or should be) the following:

Mathematics is a vast body of knowledge.  To ensure the continuing 
survival (esp. correctness) of this knowledge, one proposal is that the
next gold standard is to type up mathematics in e.g. Lean, rather than LaTeX.  

This is a reasonable idea (if what Kevin Buzzard says is true), BUT introduces 
"community service” into math: every mathematician expends some effort 
(formalising their stuff) for the greater good (that math remains reliable).  

There are however possible advantages to the individual mathematician too: 
there is ever-developing TECH (as Harvey puts it) that can take some grunt 
work off the hands of the individual mathematician.  And perhaps math 
departments will have some “typists” again who formalise math for those 
resisting the “coming tide” (as Kevin Buzzard is wont to put it).

For Kevin Buzzard et al, note that you are up against the following non-scientific obstacle:  

Working in the other exact sciences generally means plenty of team work 
and therewith some kind of “community service” (writing proper code, 
documenting your experiments, …).  This is far less the case in mathematics, 
for various reasons not  relevant here.  This greater level of individualism is an 
obvious obstacle as people generally do not feel as much responsibility for the 
bigger picture.  

Best,

Sam

PS:  Another argument pro formalisation that Kevin Buzzard et al may put on the table:  

at one point, it was realised that the general definition of continuity used in E. Bishop’s
constructive analysis was faulty and needed to be changed/fixed.  F. Waaldijk has written on this,
I believe, but this is not exactly advertised on the front page.  Similarly, the definition of real number
in early RM was wonky, and this is only mentioned in passing in the literature (see p. 78 of SOSOA).  

There are probably many examples of this kind of thing (swept under various carpets), and one
cannot hope to put together a large system of knowledge without running into these problems.  
Kevin Buzzard et al (merely) suggest we should use formalisation as a way to thwart these problems.  


> On 1 Mar 2021, at 03:57, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> On Sun, Feb 28, 2021 at 9:08 PM <dennis at logicalphalluses.net> wrote:
>> 
>> 
>>> a formal system S and a sentence phi, and the problem is to prove phi from S
>> 
> 
> DENNIS
> 
>> You seem to equate "proof assistants" (ITPs) with "automated theorem
>> provers" (ATPs). Proof assistants assist with proving, they don't do the
>> proving (entirely) for you. Almost every proof assistant contains some
>> or several ATPs for convenience, but some don't (e.g. metamath).
>> 
>> I think you're making a mistake by measuring the success of ITPs merely
>> by how powerful they are as ATPs.
> 
> ME
> 
> I tried to make clear what I was trying to do by seeing what can be
> done with the proof technology AS PURE AUTOMATED UNAIDED DEDUCTION.
> 
> The reason I am trying to do this is to UNDERSTAND THE JUMPS THAT THE
> TECH IS ABLE TO MAKE.
> 
> In a real situation, one has vast libraries and special decision
> procedures and the kitchen sink to use in order for the tech to prove
> something new.
> 
> BUT if the tech is going to do ANYTHING LIKE what people who think
> (wrongly I think) that Proof Assistants are really going to make a
> difference with Garden Variety Professional State of the Art
> Mathematical Advances - other than LIMITED SPECIAL THINGS WE ALL SEE
> THE TECH DO, the Tech is going to have to make SERIOUS JUMPS.
> 
> So I was trying to find UNCLUTTERED situations where it is a matter of
> PURE JUMPS.
> 
> Of course I am aware that any Library has for decades had those PA
> examples as an integral part. AND the most elemental of what I was
> looking at is in the language of PRESBURGER and so decision packages
> are available for them. Also there are extended decision packages
> which certainly cover NO SQRT(2). BUT what is the most general kind of
> statement that they cover?
> 
> DIGRESSION. What is the most powerful decision procedure we have for
> arithmetic statements that goes into ring statements (i.e., beyond
> Presburger) and covers things like NO SQRT(2)? I.e., what are some of
> the really powerful and understandable decision procedures out there
> for fragments of arithmetic?
>> 
> For my own work, I pretty much know when Tech is going to be useful.
> 
> I have from time to time made the following move: IS THE FOLLOWING
> TRUE FOR ALL *SMALL* CASES?, whatever I am looking at. However, that
> is not the typical thing that I do although I plan to do more of it.
> 
> FOR EXAMPLE, I had a project which got some traction, but has since
> FALLEN THROUGH THE CRACKS.
> 
> QUESTION. ARE ALL SMALL DIOPHANTINE EQUATIONS PROVABLE OR REFUTABLE IN
> (FRAGMENTS OF) PA?
> 
> FIrst of all, some simple TECH is useful to organize and compile these
> small equations. But it would be useful for the TECH to automatically
> search for solutions to get rid of the easy ones so I can concentrate
> on the interesting ones.
> 
> But how about this problem?:
> 
> FIND A FUNDAMENTALLY BASIC SIMPLE QUESTION AT THE LEVEL OF GIFTED HIGH
> SCHOOL STUDENTS, IN THE INTEGERS OR RATIONAL NUMBERS, THAT CANNOT BE
> ANSWERED IN THE USUAL ZFC AXIOMS.
> 
> I submit to you that TECH is not going to help with this. Of course
> TECH can be used to formally verify my work on this, but WAY WAY WAY
> WAY after I have very polished complete manuscripts with my personal
> proofs.
> 
> Harvey Friedman