On: LeanDojo: Theorem Proving in Lean Using LLMs

[bubblyworld]

You don't need to implement a diagonalisation in order to prove results about it - this is true for computers as much as it is true for humans. There are formalisations of Godel's theorems in Lean, for instance. Similarly for arguments involving excluded middle and other non-constructive axioms.

I hear your point that humans reason with heuristics that are "outside" of the underlying formal system, but I don't know of a single case where the resulting theorem could not be formalised in some way (after all, this is why ZFC+ was such a big deal foundationally). Similarly, an AI will have its own set of learned heuristics that lead it to more rigorous results.

Also agree about minds and computers and such, but personally I don't think it has much bearing on what computers are capable of mathematically.

Anyway, cheers. Doesn't sound like we disagree about much.

[paraschopra → bubblyworld]

what is the basic intuition of how godel's theorem are proven in Lean?

I understand OP's point of diagonalization proof being impossible to prove on a computer. (Did I get this right?)

[housecarpenter → paraschopra]

You can absolutely formalize proofs using diagonalization arguments on a computer in just the same way you would formalize any other proof. For example here's the Metamath formalization of Cantor's argument that a set cannot be equinumerous to its power set: https://us.metamath.org/mpeuni/canth.html

In mathematics we often use language to talk about a hypothetical function without actually implementing it in any specific programming language. Formal proofs do exactly the same thing in their own formal language.

Although in the case of Cantor's diagonal argument, I don't know in what sense any function involved in that proof would even fail to be implementable in a specific programming language,. Let's say I encode each real number x such that 0 <= x < 1 in my program as a function which takes a positive integer n and returns the n'th digit of x after the decimal point. In Python syntax:

    from typing import Callable

    # PosInt, Zero and One aren't built-in Python types but just assume they are
    Number = Callable[[PosInt], Zero | One]

    Sequence = Callable[[PosInt], Number]

The function involved in the diagonalisation argument can then be implemented as follows:

    def diagonalize(sequence: Sequence) -> Number:
        def diagonal(n: PosInt) -> Zero | One:
            if sequence(n)(n) == 0:
                return 1
            else:
                return 0
        return diagonal

The argument consists of the the observation that whatever sequence you pass as an argument into "diagonalize", the returned number will not be present in the sequence since for every positive integer n, the n'th digit of the returned number will be different from the n'th digit of the n'th number in the sequence, and hence the returned number is distinct from the n'th number in the sequence. Since this holds for every positive integer n, we can conclude that the returned number is distinct from every number in the sequence.

This is just a simple logical argument---it wouldn't be too hard to write it down explicitly as a natural deduction tree where each step is explicitly inferred from previous one using rules like modus ponens, but I'm not going to bother doing that here.