On the adoption of formalised math

[Carette, Jacques]

As Mathematics is not just about proof, readers of FOM might also be interested in
Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge, J. Carette, W.M. Farmer, M. Kohlhase, F. Rabe
The Mathematical Intelligencer (2020)
https://doi.org/10.1007/s00283-020-10006-0
(it's open access, so all can download it)

Tool support can help with many of the different aspects of mathematics. For example, our students and fellow mathematicians would benefit greatly if we paid as much attention to narrative as we do to proof.

Jacques

> -----Original Message-----
> From: FOM <fom-bounces at cs.nyu.edu> On Behalf Of Sam Sanders
> Sent: March 2, 2021 3:32 AM
> To: Harvey Friedman <hmflogic at gmail.com>; Buzzard, Kevin M
> <k.buzzard at imperial.ac.uk>
> Cc: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: On the adoption of formalised math
> 
> 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