3 ms·

I rather read some thing that's formal and readable, than just merely readable. > One thing I would be interested in is an objective look of how the limitation

I rather read some thing that's formal and readable, than just merely readable. > One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot. ~Goëdel~ Gödel's theorems are not relevant. Consider even if the halting problem had the other answer, it still could be impractical to do the brute force search. Same thing here. And frankly, the formal methods community is sick of people spreading FUD from that stuff. Mixing romantic humanism with technical misunderstandings is no good.

hollerith 5y ago
It is spelled Gödel or (in case you cannot put the 2 dots over the "o") Goedel.
- Ericson2314 5y ago
  Yes thank you. I guess I mixed up US keyboard vs phone typing rather hilariously.
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 ago
  I 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 ago
    Thanks 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 ago
  Foundations 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 :-)
nomoreplease 5y ago
> Mixing romantic humanism with technical misunderstandings is no good. What are you referring to with this comment?

hollerith 5y ago

It is spelled Gödel or (in case you cannot put the 2 dots over the "o") Goedel.

Ericson2314 5y ago
Yes thank you. I guess I mixed up US keyboard vs phone typing rather hilariously.

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 ago
I 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 ago
  Thanks 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 ago
Foundations 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 :-)

nomoreplease 5y ago

> Mixing romantic humanism with technical misunderstandings is no good. What are you referring to with this comment?