We're talking past each other for some reason. I'm not "unhappy" with anything. I just pointed out that (1) a result like this requires peer review by a professional human mathematician, which fundamentally bottlenecks progress in a pretty severe way; (2) such review would not be necessary if it were accompanied by a formal Lean artifact; (3) you can have both a formal proof and an informal proof together (one does not rule out the other); (4) searching for proofs formally first, then translating successful auto-verified proofs into natural language, is the most scalable approach in the near future for AI mathematics; (5) AI conjecturers would likely benefit from the results of (4) for making large leaps and connections, which can then scale into formal proofs for verification, which then feed back into the same loop ...; (6) humans guide this process through taste, judgment, and their own intuition, likely often intervening to ensure that the loop is aligned and producing a body of conceptual informal mathematics that is valuable to humanity.