#proof complexity

When an AI thinks about an problem and figured out the idea to solve it, there are a couple cases for the solution.

Case 1) It already knows the solution. It just presents the solution near instantly.

Case 2) If it synthesises n different ideas together linearly, like a chain of logical deduction with n axioms in use along the way, it can arrive at the solution. The n ideas needed are probably whatever the question is about. The AI already knows each of these n ideas in the way mentioned in the previous case. This is somewhat like applying a known theorem to a problem.

Case 3) If it needs to chain asymptotically more than n ideas to get the solution (like n^{2} ideas or e^{n}). Once all of these sub problems are solved, this reverts back to a Case 2 problem. While there are different algorithms, like nlogn or n!, that I could use to describe the problems that fit into this case, and I’m sure I could extend these categories infinitely by picking bigger and bigger algorithms, I don’t think it really matters how much further over n it is, since it all depends on what the AI already knows. The point is that problems in this category require solving sub problems.

Currently I feel like AI and LLMs are stuck at the level of category 2, and probably only for low values of n. I’m thinking of this as something like halfway up the category.

I think once they get into the level of category 3, where they’re not just applying information we already know but sort of synthesising it themselves, that’s when we get a runaway AGI effect, since they can perform research on themselves.

It’s also interesting to think about the recursive nature of discovery and invention and research. You should really be able to solve any problem by applying the method in category 2 to it, and attempting to guess what ideas you’d need to prove for each stage and checking their validity via the exact same method.

I think AIs current limitations on this are probably things like the context window (so they forget stage 1 once they hit stage 17) and perhaps the ability to recursively apply this idea. I don’t know enough about how they’re training the models to say if they’ve been trying to implement this recursion or not, although I assume they have, as this is a pretty obvious idea to try.

What I do think the AIs are pretty good at right now is guessing what ideas might be useful to try and prove. I’m sure they could be better, but it’s impressive they’ve risen to essentially my level at this task. To be fair though, the AI typically goes for the most surface level answer possible, and doesn’t try to get deeper into a topic unless prompted. This lack of curiosity might be a downside too. They certainly know enough and can think clearly enough to come to these conclusions, but they can’t be bothered to since a standard answer is just as well received generally.

anime girl proof complexity! ANIME GIRL PROOF COMPLEXITY!

Proof Complexity workshop in Oxford, 2025

This week I've been lucky to attend my first workshop outside of my home country, learning about proof complexity and bounded arithmetic. The first day left me feeling the biggest imposter syndrome in my life as I was getting lost in most of the talks but luckily during the other two days there were more talks about topics I was familias with and the last day, my friend gave a talk closely connected to forcing with random variables and I was ecstatic that I was able to understand that one without any problem. The last years Student Logic Seminar paid off.

Igor Oliveira's survey article on the main results from complexity theory and bounded arithmetic is a good starting point if you're interested in these topics.

The Complexity Zoo for information on complexity classes. (For pdf version click here.)

The Proof Complexity Zoo for information on proof systems and relationships between them.

Computational Complexity blog for opinions and interesting blog posts about computational complexity and bunch of other stuff.