Another Step Towards Optiland

When the Clay Mathematics Institute announced the Millennium Prize Problems back in 2000, we joked that if you proved P = NP, you wouldn't only get the $1 million prize for solving P v NP, but you would get $7 million since you could use P = NP to solve the rest.In theory, if P = NP, then you could efficiently find the proof of any theorem, provided its formal proof was not too long. In practice, we don't have P = NP, and back then we didn't even have a good way to formalize a proof. Fast forward to today and we have a computer generated formalized proof of Navier-Stokes and a number of other important problems.In my 2022 CACM article, I argued that we were heading towards Optiland, where we got all of the goodies of P = NP, without losing cryptography. But some challenges remained.Machine learning seems to fail learning simple arithmetic—for example, summing up a large collection of numbers or multiplying large numbers. One could imagine combining machine learning with symbolic…

Commenting on Bubbles has been removed. Why? If you want to talk about this post, write to the author, use the comments on their blog if it has them, or reply with a "RE:" post on your own blog. Suggestions? feedback@bubbles.town