For example, if the statement to be proved is say independent of ZFC, then no computer that can be computed from a Turing Machine (which includes all LLMs) can resolve the conjecture, and due to independent statements, you can make conjectures that are arbitrarily hard to solve, and even the non-independent conjectures may in practice be unsolvable by any human or AI for a long time, which means the benchmark is less useful for real AIs.
I don’t believe this is true, actually! What do you mean by “resolve the conjecture”? If you mean write up with a proof of it, then of course you can write a turing machine that will write a proof of the conjecture, it’s just infinite monkeys. ZFC is best thought of as the “minimal set of axioms to do most math”. It’s not anything particularly special. You can have various foundations such as ETCS, NF, Type theory, etc. If we have a model that can genuinely reason mathematically, then the set of axioms the model uses should be immaterial to its mathematical ability. In fact, it should certainly be able to handle more or less axioms, like replacing full choice with countable choice etc. Maybe I misunderstood your point here.
While I am not experienced at all in formalizing math, and thus am willing to update and be corrected by any expert on mathematics, especially those that formalize mathematics in proof assistants, I’d expect 2 language independent reasons for why formalizing mathematics in proof assistants are difficult:
But my point was that there are things that should be extremely easy, like proving lemmas about elementary row transformations, that have not been done in Lean yet. That is not due to a lack of people formalizing, but due to fundamental limitations with the proof assistant. The point that I’m failing to make explicit is that this seems like a copout. The ultimate naturalistic benchmark for an LLM’s math ability is being able to formalize the undergraduate math curriculum! But it starts with having a proof assistant that is amenable to the formalization project, which seems to be the bottleneck today.
I don’t believe this is true, actually! What do you mean by “resolve the conjecture”? If you mean write up with a proof of it, then of course you can write a turing machine that will write a proof of the conjecture, it’s just infinite monkeys. ZFC is best thought of as the “minimal set of axioms to do most math”. It’s not anything particularly special. You can have various foundations such as ETCS, NF, Type theory, etc. If we have a model that can genuinely reason mathematically, then the set of axioms the model uses should be immaterial to its mathematical ability. In fact, it should certainly be able to handle more or less axioms, like replacing full choice with countable choice etc. Maybe I misunderstood your point here.
But my point was that there are things that should be extremely easy, like proving lemmas about elementary row transformations, that have not been done in Lean yet. That is not due to a lack of people formalizing, but due to fundamental limitations with the proof assistant. The point that I’m failing to make explicit is that this seems like a copout. The ultimate naturalistic benchmark for an LLM’s math ability is being able to formalize the undergraduate math curriculum! But it starts with having a proof assistant that is amenable to the formalization project, which seems to be the bottleneck today.