AlphaProof Code

Re:AlphaProof Code by xrisk on Tuesday November 10, 2026 @07:31AM (#50439411)

lean has no relation to the halting problem; you can think of it as a language that allows proofs to be encoded as code, and the compiler that runs that code as knowing how to enforce mathematical constraints appropriately

[ Parent | on HN ]

Re:AlphaProof Code by auggierose on Tuesday November 10, 2026 @07:38AM (#50439477)

there certainly is a relation; you might not be able to prove all the properties you care about because of the halting problem; but that is more a theoretical problem, not a practical one

[ Parent | on HN ]

Re:AlphaProof Code by gf000 on Tuesday November 10, 2026 @08:30AM (#50440025)

> you might not be able to prove all the properties you care about

And just to add, this is also true of "human" mathematics as well.

[ Parent | on HN ]