3 ms·
I didn’t mention Goedel’s theorems, so I don’t know what they’re relevant or irrelevant to, and I am not spreading anything. Maybe I didn’t make that part clea
by bmitc 5y ago
I didn’t mention Goedel’s theorems, so I don’t know what they’re relevant or irrelevant to, and I am not spreading anything.
Maybe I didn’t make that part clear, but it’s more of a question of mine than a statement. It seems to me there would be problems and limits but I haven’t seen them addressed in a way I understand, so the questions and misunderstandings remain.
If you have any references, then by all means share them.
> Mixing romantic humanism with technical misunderstandings is no good.
I think this miscategorizes what I wrote. One could easily do the same.
Mathematics is indeed a human endeavor, as are its goals. If machines are to help, then that’s absolutely great (I’m actually a big fan of computers being used to augment human endeavors), but making grand sweeping claims like I’ve seen in discussion of proof assistants is as romantic as anything.
- foxes 5y agoI think the proof assistants are getting very powerful, eg: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... State of the art research explored with lean. I think a certain level of hand wavy romanticism is fine for a HN comment if it can inspire people to be interested in the field. I also would prefer to be corrected in a reasonable discussion than a silent chilling downvote.
- bmitc 5y agoThanks for the article/interview. I am intrigued to find Peter Scholze’s own words calling this a “human experience”. https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/#comment-2299 https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... This is actually a great article that helps to show that humans are still very much involved in convincing each other, using machines to aid to that effect. Regarding downvotes, you can’t even downvote someone you’ve replied to or they’ve replied to you on Hacker News.
- ProfHewitt 5y agoFoundations of mathematics are inferentially incomplete, that, is, there are true but unprovable propositions (although [Gödel 1934] results do not hold for foundations). See following for a proof: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 However, inferential incompleteness does not cause practical difficulties for proof checking assistants :-)