“Practical” sounds like you care more about guaranteed correct results than about understanding how you got them. If you want a “practical” proof, why isn’t it better to produce something that a mechanical checker can verify than to produce something legible to a human?
An annoying thing about current chatbots is that even when they’ve plausibly solved a math problem, they often can’t explain the solution (a proof explains truth of a proposition). Legible informal proofs are also more central to math than rigor or even correctness. Math is about understanding, occasionally you end up understanding something without yet being able to make it rigorous, and initial attempts at making it rigorous make it incorrect, but eventually it can be made correct in some other setting (that in principle might need to be invented first).
“Practical” sounds like you care more about guaranteed correct results than about understanding how you got them. If you want a “practical” proof, why isn’t it better to produce something that a mechanical checker can verify than to produce something legible to a human?
An annoying thing about current chatbots is that even when they’ve plausibly solved a math problem, they often can’t explain the solution (a proof explains truth of a proposition). Legible informal proofs are also more central to math than rigor or even correctness. Math is about understanding, occasionally you end up understanding something without yet being able to make it rigorous, and initial attempts at making it rigorous make it incorrect, but eventually it can be made correct in some other setting (that in principle might need to be invented first).