This question resolves when an AI first gets IMO Gold. It resolves YES if this AI is explicitly coded to do the following:

1. Receive as input (or construct using natural language processing), problems which take the form of mathematical propositions encoded in a formal language.

2. Construct a tree of logical transformations of that initial proposition (e.g. in the form of tactic applications), and iteratively extend this tree with the goal of identifying a subtree which comprises a complete formal proof of the proposition.

Note that an AI which is not coded to do this explicitly, but instead identifies this strategy emergently does not count.

For example, an AI as described in the paper "HyperTree Proof Search for Neural Theorem Proving" would satisfy these conditions.

Close date updated to 2030-12-31 3:59 pm