News for hackers. Stuff that matters.

A comment on Why the Legendary Erdős Problems Are Falling to AI. Parent comment

Re:Why the Legendary Erdős Problems Are Falling to AI by stymaar on Wednesday August 05, 2026 @11:45AM (#49184513)
> The vast majority of it could be inscrutable, ugly, chaotic and seemingly meaningless.

It is, provably: per Curry–Howard correspondence, any program you write is a proof of a theorem, and it is indeed mathematically meaningless.

[ Parent | on HN ]
Re:Why the Legendary Erdős Problems Are Falling to AI by inigyou on Wednesday August 05, 2026 @12:06PM (#49184767)
Generating a value of type "Either (Int, String) Bool" is proving that there's at least one integer and at least one string, or there's at least one valid boolean value. Except in Haskell, where it could also be an infinite loop.
[ Parent | on HN ]