I saw this analogy made comparing AI finding proofs to open mathematical conjectures with AI constructing a model that finds a compound for treating cancer and statistically predicting that it would pass a Phase III clinical trial.

This seems like a problematic comparison to me because finding a proof to a conjecture is not the same as making a prediction with a statistical model. No matter how good a prediction is on paper, it is still no reason to treat that compound as though it had already passed Phase III (or even Phase I). On the other hand, a proof to a conjecture can be directly checked if it is right or wrong; there is no uncertainty to it. If the proof compiles on Lean, then it means that it is correct in as far as what being correct from compiling on Lean means.

Of course, an AI finding a compound that it predicts will pass a Phase III trial is still informative.…