The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen. People will just put up the formally verified result and call it a day, and there's no incentive for them or anyone else to clean things up.
We'll end up with incomprehensible math because comprehensibility isn't rewarded. No one is going to get a Fields Medal, or tenure, for digesting someone else's results.
> The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen.
He says it shouldn't be able to published if they can't explain it. Publishing it is the reward.
> People will just put up the formally verified result and call it a day, and there's no incentive for them or anyone else to clean things up.
The incentive will be to be able to publish in a top tier journal. I suspect what Tao is advocating for is having journals reject such manuscripts.
> No one is going to get a Fields Medal, or tenure, for digesting someone else's results.
I'm sure no one gets a Field's Medal if others can't digest their results.