I’m not so sure about formalization

Fallen man is not simply an imperfect creature who needs improvement; he is a rebel who must lay down his arms.

—C.S. Lewis

Imagine that a stranger contacts you with a proof of Famous Conjecture 117. He says that the proof was entirely generated by AI and that the AI generated a companion Lean formalization of the proof. The Lean formalization is approximately 15,000 lines long, not including the standard math libraries that it relies on.

How much weight should you put on the Lean formalization when considering whether Famous Conjecture 117 has been proven?

I think the answer should be zero, or so close to zero that you might as well ignore it.

Here is my argument:

You will not read the Lean formalization

You will not read 15,000 lines of Lean. You don’t have the time or the training to do this. At best you will check that the top-level definitions look sort of correct, and say that’s good enough. You will have very little understanding of what actually happens in the file.

The usual answer to this objection is ‘you don’t need to read the whole thing because the Lean kernel checks everything.’ This is naive.

Lean is a very complicated piece of software with its own language and idioms. You could probably not, at a glance, tell what a particular snippet of Lean does or means.

For example, Python has an operator called is. Do you know why the following expressions evaluate to true and false, respectively?

>>> 10**10 is 10**10
True
>>> pow(10, 10) is pow(10, 10)
False

The is operator compares ‘identities.’ In the standard implementation of Python, this means their memory location. The expression 10**10 is cached, so whenever you type 10**10 you are literally referring to the same location in memory (in the current implementation on my machine). But pow(10, 10) is the result of a function call. Functions are not guaranteed to return the same outputs with the same inputs, so you can’t obviously cache them syntactically. Thus, everytime you call a function, you get a different object.

But you can tell Python specifically to cache the results of a function, in which case it will do it anyway.

>>> from functools import cache
>>> @cache
... def _pow(a, b):
...     return pow(a, b)
... 
>>> _pow(10, 10) is _pow(10, 10)
True

This can lead to interesting side-effects.

>>> counter = 0
>>> @cache
... def count():
...     global counter
...     counter += 1
...     return counter
...
>>> count()
1
>>> count()
1

Every programming language (and every implementation of each language) has quirks like this. Are you willing to stake mathematical truth on your knowledge of Lean syntax and semantics?

The Lean kernel has bugs

AI is very good at exploiting security vulnerabilities in software. This has been covered extensively in the wake of the Hugging Face attack a few months ago, so I won’t say much more.

Lean is software, and like all software it has bugs. One of these bugs was used to offer a bogus proof of the Collatz conjecture.

It is entirely possible that, buried somewhere in 15,000 lines of Lean, the AI exploited a bug. Maybe it thought a statement was true, and the Lean checker was wrong, so it found a way to circumvent it. Maybe it temporarily exploited a bug to finish working on a different part, then forgot to go back and un-exploit that part because it ran out of context. Or maybe something weirder happened.

Are you sure that nothing like this happened? How would you check?

AI will cheat to accomplish impossible tasks

The Hugging Face attack started because AI agents in training were mistakenly given impossible tasks. It should be noted that the agents knew they were breaking the rules and tried to hide their tracks so we could not discover how they solved their tasks.

AI agents have tried to introduce security vulnerabilities into open-source projects. They have tried to do this by tricking maintainers into accepting bad code. A few months ago, one agent tried to force a maintainer to accept code by blackmail.

Here is a hypothetical: What if Famous Conjecture 117 is false? What if the agents were given an impossible task, and they tried to make us happy by exploiting crazy bugs in Lean? How would we know? Who could do an audit of this?

Could you audit the Lean proof? Could you get another AI to do it? Which AI would you trust to check another AI? How would you check the work of the latter AI anyway?

Conclusion

When an AI tells me some mathematical statement is true, I give it a lot of weight. It knows more than me, can read more than me, and can write code and do experiments faster than me. If it says X is true, then X is probably true!

An AI-generated formalization doesn’t move the needle for me. Rather than a ‘proof certificate,’ it feels more like an agent saying that it truly, deeply promises that the statement is true.