10 ms·
A hundred pages of impenetrable brute forced Lean would advance the field much less than something elegant and human understandable, perhaps relying on some new
by qlte 8d ago
A hundred pages of impenetrable brute forced Lean would advance the field much less than something elegant and human understandable, perhaps relying on some new clever spark of innovation that might inspire new areas of research.
Particularly if the first proof being "solved" thanks to piles of money and compute for self-serving marketing discourages the mathematician who might have otherwise devoted years of focus to reach the superior proof we will now never see.
- semi-extrinsic 8d agoObtaining a finite-time blow-up for Navier-Stokes does not necessarily advance the field of mathematics by any significant measure, whether the proof is very long or very short. As a concrete example, such a proof could be less than a page with very specific initial and boundary conditions and inserting them into the equations to get something that goes to infinity when time goes to some finite value. This would resolve the Millenium problem but not make humanity any smarter.
- gw32 8d agohttps://mathstodon.xyz/@tao/117207849921390904 https://mathstodon.xyz/@tao/117207849921390904 Tao agrees.