[FOM] Foundational Challenge

[Emilio Jesús Gallego Arias]

Dear all,

Joe Shipman <joeshipman at aol.com> writes:

> None of this comes close to giving a positive answer to my challenge,
> and I’m not interested in changing the subject, because my challenge
> is intended to address the PRACTICAL question “would an ordinary
> mathematician whose primary interest is in finding and proving
> theorems become any more effective at doing so by using an alternative
> foundation than ZFC (plus large cardinals if necessary)?”

> If no positive answer to my challenge is forthcoming, I conclude that
> the only mathematicians who might need to care about alternative
> foundations are those working in areas of math that relate directly to
> the alternative foundation.

The first that came to my mind when reading the challenge was "how would
a formal/complete proof of the 4-color theorem would look in ZFC" ?

Do you think Gonthier's proof [1], as done in the CIC type theory does
qualify to improve the ZFC version?

I'm unsure I know how to answer that question, and whether type theories
would be considered to be related directly to the area of mathematics
doing proofs with large computational content.

Kind regards,
Emilio J. Gallego Arias

[1] https://www.ams.org/notices/200811/tx081101382p.pdf