Post

In his book, "The Proof in the Code: How a Truth Machine Is Transforming Math and AI," @kevinhartnett.bsky.social tells the story of computer program Lean in an effort to answer a longstanding question: Can computers reveal universal truths? Out today from @quantabooks.org: https://bit.ly/43X5To1

"Truth Machine". Now, that's.. a lot. Gödel is cancelled? Did I miss the memo? bsky.app/profile/simo...

What exactly do you think Gödel has to do with this?

not sure if you are up to speed but they invented libraries. they have these things called books. they're great.

Well, so I am going to have to ask which one of Gödel's theorem the post was referring to then?

the fact that that is your response kind of indicates that you didn't appreciate what the whole deal was with Godel, namely that it nuked ANY attempt to logic yourself out of the question of knowledge. so, the whole posture of this guy is ridiculous regardless of the specifics.

sorry, get overly annoyed by the idea that people find an idea like "truth machine" even remotely worth pondering over for more than two second. my bad. i thought "godel is cancelled?" was a pretty good way to pre-empt such pondering.

Of course the guy is doing some kind of marketing, but type theory -- which is what is behind Lean -- actually is a real thing (for instance, Lean is mostly inspired by Rocq which has been a real topic of academic research for over 30 years (especially in France)).