Post on Formal Conjectures Benchmark

Stream: Formal conjectures

[Franz Huschenbeth]

I have written a popularizing Post on the Formal Conjectures Benchmark, or viewed more generally using open math problems in Formal Proof Systems as a Benchmark.

The general intended audience, is people not necessarily knowing Lean / Formal Proof Systems (or not even being deep in Math for that matter), but are still interested in these sort of topics. It can also be read by someone knowing Lean, I did not in cover Lean in detail.

If you have the time, I would love to hear some Feedback, before I try to distribute it. You can take a look at it here.

[Bolton Bailey]

nT is likely quite big

Is there a particular reason you think this is true? In the Aaronson survey you cite, nT is conjectured to be under 20 for ZF, which doesn't seem that big to me.

[Franz Huschenbeth]

I did not mean big in the sense of an integer, but big in the sense that it will be sufficiently big for measuring the intelligence of AI. If we create an AI System, which will be able to hit that barrier, then we have an AI, which is vastly (vastly) more intelligence than us.

So I meant it more in the sense, that it is big as it will be very (very) hard to proof all Busy Beaver values up to that constant nT.

Will correct / clarify it in the post. Thanks for the Feedback :)