Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.
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.
If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever.
Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.
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.
4 replies →
Why not both? Not sure why you're presenting this as one or the other.
What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.
If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever.
3 replies →