It’s been an interesting few weeks for counterexamples. This post is basically my perspective of what has been going on in the world of formalization, AI tools and, in particular, counterexamples.

Crazy shit, dog.

Whatever happens, the real danger is not that AI will become too good, but that it will become too evil—most likely because of the oligarchs, corporations and governments behind it. I wish I had emphasized that point, which is always on my mind.

I think I succeeded in making another point, which is that life will not become pointless simply because some other entity gets better than humans at something and knocks us off our throne. To think that the meaning of life resides in our superiority is a childish attitude.

It seems to me that we’re now over the top of this particular rollercoaster, and it will keep accelerating until we reach the bottom, wherever that might be. I don’t know whether to hope or dread that solutions to P versus NP and all our other great problems will be included in the ride—that our role, as human mathematicians, will be reduced to (at most) deciding which questions we find interesting and then understanding AI models’ answers to those questions.

But maybe that won’t happen. Maybe the new AI mathematicians will soon hit a wall, because they lack the uncomputable quantum gravity microtubules of Penrose and Hameroff, or some other magic human ingredient. The fantastical thing is that, one way or the other, we’re going to find out empirically before very long.

A collection of notes/courses covering linear algebra, calculus, leading to AI

Terry Tao gives a detailed description of exactly how to use Lean to formalize a proof.