[bubblyworld]

To be pedantic (mathematical?), computers can find any result that has a formalisation in a finitary logical systems like first-order logic, simply by searching all possible proofs. Undecidability of FOL inference isn't relevant when you already know such a proof exists (it's a "semidecidable" problem).

I imagine that would be the main use case for heuristic solvers like this one - helping mathematicians fill in the blanks in proofs for stuff that's not too tricky but annoying to do by hand. Rather than for discovering novel, unknown concepts by itself (although I'm with the OP, don't see why this is impossible a priori).

[mathinaly]

Because meta-mathematical proofs often use transcendental induction and associated "non-constructive" and "non-finitistic" arguments. The diagonilization argument itself is an instance of something that can not actually be implemented on a computer because constructing the relevant function in finite time is impossible. Computers are great but when people say things like "The human mind is software running on the brain like a computer" that indicates to me they are confused about what they're trying to say about minds, brains, and computers. Collapsing all those different concepts into a Turing machine is what I mean by a confused ontology.

In any event, I'm dropping out of this thread since I don't have much else to say on this and it often leads to unnecessary theorycrafting with people who haven't done the prerequisite reading on the relevant matters.

[skissane]

> Because meta-mathematical proofs often use transcendental induction and associated "non-constructive" and "non-finitistic" arguments. The diagonilization argument itself is an instance of something that can not actually be implemented on a computer because constructing the relevant function in finite time is impossible.

Humans reason about transcendental induction using finite time and finite resources-the human brain (as far as we know) is a finite entity. So if we can reason about the transfinite using the finite, why can’t computers? Of course they can’t do so by directly reasoning in an infinite way, but humans don’t do that, so why think computers must?

[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]

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]

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.