On 1/25/20 6:04 AM, Jon P wrote:
I also think the future of mathematics lies in formal proofs.
I've been (pleasantly) surprised to find that at least occasionally the PRESENT of mathematics lies in formal proofs.
From the preface to the HoTT book: 'The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human be- ing, as a complement to a formal proof that can be checked by a machine. . . . much of the material presented here was actually done first in the fully formalized setting inside a proof assistant, and only later “unformalized” to arrive at the presentation you find before you — a remarkable
inversion of the usual state of affairs in formalized mathematics.' -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f4e1b6a3-0398-a71e-c32f-5deaddf015af%40panix.com.
