[FOM] Improving Set Theory/Self Proving

[Harvey Friedman]

I was referring more to sociological/practical issues. I was reading
this from a source who is a working expert in Proof Assistance. I just
can't recall the reference.

The idea I read is that "it is virtually impossible to get funding
agencies to see enuf need to grant the required resources to get, say,
FLT formally verified with the best arguments for what is to be gained
by doing so". And "we have already established that size and deep is
not an in principle obstacle to the formalization thesis. So it can
argued that not too much is gained by pushing the size and complexity
of the math further up that is seen to allow rigorous formalization".
And I was remarking that this is not the case for program and
engineering system verification because there one can argue economic
gains and security gains of various kinds that cannot be remotely
argued for verifying big deep mathematics.

Perhaps somebody on FOM can recall a good place where this is discussed.

Hence my proposals concerning "self proving" and "level of ideas" in
https://cs.nyu.edu/pipermail/fom/2020-January/021884.html   concerning
 , in order to put more juicy foundational theory on the bones. It
also discusses Make Set Theory Great Again of John Harrison.

On Mon, Jan 13, 2020 at 8:22 PM Timothy Y. Chow
<tchow at math.princeton.edu> wrote:
>
> Harvey Friedman wrote:
>
> > I gather from some comments I have seen that there is a bit of a crisis,
> > with regard to Proof Assistants aimed at creating formal proofs.
> >
CHOW
> I'd be curious to hear more about this alleged "crisis."
>
> There are various possible obstacles to scaling up from the current
> situation to a situation where all or most of mathematics is routinely
> formalized.
>
> For example, there are sociological obstacles that have next to nothing to
> do with the technical merits of proof assistants.  There is very little
> reward, in terms of jobs, awards, and promotions, for learning how to use
> a proof assistant and formalizing proofs of one's own theorems in them.
> Also, the existing documentation is still poor, at least from the point of
> view of a mathematician.