6 ms·

I don't think Gowers is trying to build a better theorem prover. An AI researcher would be trying to build a better prover. Gowers is a mathematician looking

by yaseer 4y ago

I don't think Gowers is trying to build a better theorem prover. An AI researcher would be trying to build a better prover. Gowers is a mathematician looking for mathematical insight. This project's success would be based on how well it answers those fundamental questions he posed (i.e How does a human generate proofs, given no algorithm exists to solve the halting problem?) The output might be more like meta mathematics, with insights provided by software, rather than ML software optimised for a goal.

amelius 4y ago
They can still use ML to prune the search space, I suppose?
- yaseer 4y ago
  For a mathematician, it's not the output of pruning the search space, but understanding how the search space is pruned. Understanding how ML models work is a notorious problem. A classical algorithm can be formally understood better - I think it's this mathematical understanding Gowers is looking for.
  - amelius 4y ago
    But isn't that how humans do it too? They have a hunch, pursue it, and if it doesn't work out, they backtrack. Of course, some people have better hunches than others, but that doesn't change the global idea.
    - jhgb 4y ago
      ...and they largely don't know where those hunches came from.
      - tsukikage 4y ago
        ...well, quite. But that's not really the "move along, nothing to see here" it first sounds like. "Hunch" is a label we use for "I don't know explicitly how I came up with this". Generally, when we have a label for a concept the description of which starts with "I don't know...", some people try and follow up with questions: is that a thing it is possible, in principle, to know? How could we find out for certain? If it's knowable, how do we get to know what it is? Sometimes, they succeed, and generations of such successes is how we end up with the modern world.
    - yaseer 4y ago
      > They have a hunch, pursue it There's a lot to unpack in just this. Can we define an algorithm to generate hunches? (mathematical intuition). Given infinite hunches, can we define an algorithm to order hunches by priority, to search? That's the kind of question they'll be thinking about using the symbolic logic/classical algorithms in GOFAI approaches.
gnramires 4y ago
> How does a human generate proofs, given no algorithm exists to solve the halting problem? To be fair, this has some trivial answers -- despite being a fascinating question. For example, given a formal proof verification system (e.g. Lean), you can search for proofs (either by brute force or hopefully using heuristics) and if a proof exists, you will find it after some finite time. The problem is that sometimes no proof exists. You may be thinking of getting "smart", and also trying to prove no proof exists in parallel. But that's just another proof, such that this recursion tower (proof that (proof that (... proof doesn't exist)) doesn't resolve. But I think overall this mostly means you should be able to accept non-existence or arbitrary proving times of proofs (maybe also a sociological problem for mathematicians!). That's of course how human mathematics works: no one now if any famous theorem (e.g. Riemann hypothesis) will be proven within some time frame, or maybe never.

by yaseer 4y ago

amelius 4y ago

They can still use ML to prune the search space, I suppose?

yaseer 4y ago
For a mathematician, it's not the output of pruning the search space, but understanding how the search space is pruned. Understanding how ML models work is a notorious problem. A classical algorithm can be formally understood better - I think it's this mathematical understanding Gowers is looking for.
- amelius 4y ago
  But isn't that how humans do it too? They have a hunch, pursue it, and if it doesn't work out, they backtrack. Of course, some people have better hunches than others, but that doesn't change the global idea.
  - jhgb 4y ago
    ...and they largely don't know where those hunches came from.
    - tsukikage 4y ago
      ...well, quite. But that's not really the "move along, nothing to see here" it first sounds like. "Hunch" is a label we use for "I don't know explicitly how I came up with this". Generally, when we have a label for a concept the description of which starts with "I don't know...", some people try and follow up with questions: is that a thing it is possible, in principle, to know? How could we find out for certain? If it's knowable, how do we get to know what it is? Sometimes, they succeed, and generations of such successes is how we end up with the modern world.
  - yaseer 4y ago
    > They have a hunch, pursue it There's a lot to unpack in just this. Can we define an algorithm to generate hunches? (mathematical intuition). Given infinite hunches, can we define an algorithm to order hunches by priority, to search? That's the kind of question they'll be thinking about using the symbolic logic/classical algorithms in GOFAI approaches.

gnramires 4y ago

> How does a human generate proofs, given no algorithm exists to solve the halting problem? To be fair, this has some trivial answers -- despite being a fascinating question. For example, given a formal proof verification system (e.g. Lean), you can search for proofs (either by brute force or hopefully using heuristics) and if a proof exists, you will find it after some finite time. The problem is that sometimes no proof exists. You may be thinking of getting "smart", and also trying to prove no proof exists in parallel. But that's just another proof, such that this recursion tower (proof that (proof that (... proof doesn't exist)) doesn't resolve. But I think overall this mostly means you should be able to accept non-existence or arbitrary proving times of proofs (maybe also a sociological problem for mathematicians!). That's of course how human mathematics works: no one now if any famous theorem (e.g. Riemann hypothesis) will be proven within some time frame, or maybe never.