Human unreadable proofs have only limited value.

I disagree. It's the only way to scale AI mathematics far beyond human mathematics. Any interesting verified result would, obviously, be rewritten back into natural language for human understanding and consumption (as well as potentially for the benefit of AI conjecturers too). You are falsely assuming that advances in formal mathematics would not feed back into similar (potentially massive) advances into informal mathematics, and I think that's simply wrong. We're just at the very, very beginning of that curve.

I think this is, in fact, inevitable. It's the exact same RL loop that allowed AlphaGo to vastly exceed the world's top human players. You can theoretically RL formal proof techniques vastly beyond human capability by removing the need for any human review for correctness. It is completely reasonable to assume that "informalization" will become a real sub-field of mathematics in the near future.

▲

varjag 3 hours ago | parent [-]

I didn't say they have no value. Just limited value. A novel readable proof that expands the horizons of human insight is certainly more valuable than a megabyte sized trychnobezoar of machine generated predicates.

▲

nilkn 3 hours ago | parent [-]

You are assuming that the latter, once autonomously discovered and verified at scale, could not simply be translated into the former, also perhaps autonomously at scale (or otherwise selectively as determined by human interest, taste, and relevance).

▲

varjag 3 hours ago | parent [-]

Well we're literally discussing a human readable machine generated proof here yet you don't seem happy with that.

	▲	nilkn 3 hours ago \| parent [-]
		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.