Hacker News new | past | comments | ask | show | jobs | submit login

I agree that Lean or Coq or something else is the future of solving mechanistic argument, but my opinion is that this has been the expectation for maybe a hundred years already and was right up there in the time of Turing and Church (and Boole and Heyting and Curry and Kolmogorov).

But compare all of mathematics to just linear algebra and specifically neural network implementations. You have a lot of people working on AI who sometimes grossly overstate the capabilities of their system and fail to understand their systems when they do succeed. I would venture that the issue is not solving problems as much as it is to understand things to the level of mastery. It is always worth it to understand something to a continually exhaustive level of detail.

I think this is what artisans are. If you can make incredible hand made books [1], then surely you have underlying skills and abilities that transfer as well? If you are a grand master chess player then you may be dismayed that computers will always beat you [2], until you use a computer yourself to beat another computer (or at the very least until you become resentful towards IBM for misleading you in 1997). [3]

[1] https://www.reddit.com/user/iostopan [2] https://en.wikipedia.org/wiki/Human–computer_chess_matches [3] https://en.wikipedia.org/wiki/Solving_chess

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact