Remix.run Logo
BeetleB an hour ago

> 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.