Theoretical computer scientists are wasting their time trying to understand AI-generated proofs

[u/amichail]

Understanding an AI-generated proof in theoretical computer science may soon be like trying to understand the assembly code produced by an optimizing C compiler. It's technically possible, but why spend time doing it when better tools can do the work for you?

Instead of having theoretical computer scientists spend weeks or months checking AI-generated proofs and trying to extract insights from them, we should publish these proofs with formal verification in Lean.

Each paper would contain an English writeup and a corresponding Lean formalization. Lean would verify the formal proof, while future generations of increasingly powerful AIs would:

• Check that the English statements accurately correspond to their Lean formalizations.
• Find mistakes or discrepancies that earlier AIs missed.
• Simplify the arguments and discover more elegant proofs.
• Extract insights about algorithms, complexity, computational models, and other theoretical concepts, then explain them to researchers in simple English.
• Generalize the results and discover connections to other areas of theoretical computer science.

The papers could be continuously improved as stronger AIs become available, while preserving earlier versions.

Given how quickly AI capabilities are improving, a theoretical computer scientist might spend six months understanding a complicated proof that an AI released a year later could explain clearly in minutes.

Why not leave that work to future AIs?

Human researchers could focus on identifying interesting computational problems, exploring applications, and developing new research directions. They could still benefit from the insights contained in AI-generated proofs without having to decipher the proofs themselves.

The goal should be to advance theoretical computer science and make its proof insights automatically accessible to humans via ever more powerful AIs.

[u/Electrical-Box-6059]

you're basically describing a world where proofs become black-box infrastructure, which is interesting but i think it misses the point of why people do theory in the first place

the understanding the product, not some secondary deliverable. if an AI spits out a proof of P≠NP but nobody can follow the reasoning, we've gained exactly nothing beyond a weird oracle. the assembly code comparison falls apart because nobody builds new compilers by staring at assembly, they understand the abstractions it. theory researchers need to grasp the structure of the argument to build on it, not just know the theorem holds

formal verification in Lean solves the correctness problem but not the comprehension problem, and punting comprehension to future AIs feels like wishful thinking dressed up as a research strategy

[u/amichail → u/Electrical-Box-6059]

Future ever more powerful AIs could extract insights from the proofs for humans. Humans don't need to read the AI proofs at all.

[u/QuackSomeEmma → u/amichail]

Why should the AIs do proofs at all?

[u/amichail → u/QuackSomeEmma]

Why should AIs cure cancer and other diseases?

[u/Y-M-M-V → u/amichail]

AIs don't cure cancer. They produce small candidate sets of solutions to hard problems (such as protein folding) that are then tested in a lab and later living models. What the AI brings to the table is reducing the search space from a huge number of possibilities to a testable number.

A proof that humans can't validate is mostly not useful.

[u/mywan → u/amichail]

I've played with AI enough to know that AIs (at present) deal in abstracting a premise. It can't judge the legitimacy of the premise itself, unless it's clearly violated by a known knowledge base. I can convince an AI of almost anything simply by setting the right premise. They can try to train it out of them, but that's impossible in general. All problems have a predicate premise, and validity requires the premise it's predicated on. That's why math has axioms, which we simply assume to be true and follow the consequences. Take the ability of an AI to follow a premise (right or wrong) and it can't operate for it's intended purpose. It just becomes a fancy dictionary.

[u/latent-manifold]

I can't agree with abdicating our responsibility of understanding. Leaving it to chance that something, somewhere, might one day finish the work for us is not what science is about.

[u/amichail → u/latent-manifold]

AI is advancing very rapidly. Waiting a few months or even a year or two for an AI to give you insights/understanding from an existing AI proof is not that long of a wait.

[u/Schoens]

Tell me you don't know how proofs work, without telling me you don't know how proofs work.

We have to spend time verifying the proofs, to ensure they actually prove what they say they prove. I'm not talking about whether they are technically valid proofs - you can write a technically valid proof that doesn't actually prove what you claim it does. LLMs make mistakes regularly, what makes you believe they don't make mistakes when writing proofs? I get code that compiles and passes a type checker, yet is still wrong, on a daily basis - the only sure way to catch those mistakes is to understand the output yourself, in addition to using other tools at our disposal, such as review via other models, automated verification, etc.

Abdicating our responsibility like you propose is foolish to the extreme at this point in time. We are nowhere near the point where LLMs can be trusted to that degree - who knows how long it will take to get there, maybe not that long, but we have no reason to jump the gun, and every reason to be exceedingly careful about doing so.

[u/UncleMeat11 → u/Schoens]

Tell me you don't know how proofs work, without telling me you don't know how proofs work.

It is incredibly remarkable that OP has been on reddit for 21 years and still has max negative karma.

[u/MirrorLake]

"Use Lean" is an odd suggestion, given that people and their LLMs are already using Lean. Theoretical CS folks are well aware of Lean and its capabilities.

FYI OP's post is flagged for me as 100% LLM generated.

[u/Akari_Takai]

Wow, an LLM-generated post that misunderstands the nature of computer science & research. How original.

[u/OlenaDoubleChecks]

Lean only verifies the formal statement, and the English-to-Lean spec gap is the hallucination problem all over again. A subtly wrong formalization compiles fine and nobody catches it. Same reason demos don't survive production.

[u/Delta-9-]

The comparison to compilers is painfully naïve. New and better compilers are producible precisely because we understand how they work. New and better math gets produced precisely because we understand the proofs.

Could AI take over that iteration and improvement? Technically, maybe. But why? From doing so, we might gain the things you say we would... But more likely, we would lose the number of researchers to reap those gains, until there are very, very few people who even have a chance at directing an AI (nevermind understanding its work). We've already seen brain drain as a direct result of access to LLMs in schools and industry, so this isn't even a pessimistic hypothetical. The pessimistic hypothetical would be "... and eventually this leads to the Butlerian Jihad or, worse, Judgement Day."

There's also the difference between "technically correct" and "good." There are millions of correct paths from San Francisco to New York City; only a few of them are efficient in fuel and time. The recent Navier-Stokes solution might have an even better solution, but if we only lean on "correctness" (pun half-intended) we may be missing out. If we don't even understand the bad solution, how can we hope to find the good solution? By feeding it to another AI? See the above paragraph.

[u/__chicolismo__]

What a shitty tedtalk