[grondilu]

"I think in the future, instead of typing up our proofs, we would explain them to some GPT. And the GPT will try to formalize it in Lean as you go along. If everything checks out, the GPT will [essentially] say, “Here’s your paper in LaTeX; here’s your Lean proof. If you like, I can press this button and submit it to a journal for you.” It could be a wonderful assistant in the future."

That'd be nice, but eventually what will happen is that the human will submit a mathematical conjecture, the computer will internally translate into something like Lean, and try to find either a proof or a disproof. It will then translate it in natural language and tell it to the user.

Unless mathematics is fundamentally more complicated than chess or go, I don't see why that could not happen.

[qfiard]

It is fundamentally more complicated. Possible moves can be evaluated against one another in games. We have no idea how to make progress on many math conjectures, e.g. Goldbach or Riemann's. An AI would need to find connections with different fields in mathematics that no human has found before, and this is far beyond what chess or Go AIs are doing.

[salamo]

Not a mathematician, but I can imagine a few different things which make proofs much more difficult if we simply tried to map chess algorithms to theorem proving. In chess, each board position is a node in a game tree and the legal moves represent edges to other nodes in the game tree. We could represent a proof as a path through a tree of legal transformations to some initial state as well.

But the first problem is, the number of legal transformations is actually infinite. (Maybe I am wrong about this.) So it immediately becomes impossible to search the full tree of possibilities.

Ok, so maybe a breadth-first approach won't work. Maybe we can use something like Monte Carlo tree search with move (i.e. math operation) ordering. But unlike chess/go, we can't just use rollouts because the "game" never ends. You can always keep tacking on more operations.

Maybe with a constrained set of transformations and a really good move ordering function it would be possible. Maybe Lean is already doing this.

[grondilu]

> But the first problem is, the number of legal transformations is actually infinite.

I am fairly certain the number of legal transformations in mathematics is not infinite. There is a finite number of axioms, and all proven statements are derived from axioms through a finite number of steps.

[hwayne]

Technically speaking one of the foundational axioms of ZFC set theory is actually an axiom schema, or an infinite collection of axioms all grouped together. I have no idea how lean or isabelle treat them.

[fspeech]

Whether it needs to be a schema of an infinite number of axioms depends on how big the sets can be. In higher order logic the quantifiers can range over more types of objects.

[4ad]

Lean (and Coq, and Agda, etc) do not use ZFC, they use variants of MLTT/CiC. Even Isabelle does not use ZFC.

[robinzfc]

Isabelle is generic and supports many object logics, listed in [1]. Isabelle/HOL is most popular, but Isabelle/ZF is also shipped in the distribution bundle for people who prefer set theory (like myself).

[1] https://isabelle.in.tum.de/doc/logics.pdf

[szvsw]

Chess and Go are some of the simplest board games there are. Board gamers would put them in the very low “weight” rankings from a rules complexity perspective (compared to ”modern” board games)!

Mathematics are infinitely (ha) more complex. Work your way up to understanding (at least partially) a proof of Gödel’s incompleteness theorem and then you will agree! Apologies if you have done that already.

To some extent, mathematics is a bit like drunkards looking for a coin at night under a streetlight because that’s where the light is… there’s a whole lot more out there though (quote from a prof in undergrad)

[hwayne]

> Unless mathematics is fundamentally more complicated than chess or go, I don't see why that could not happen.

My usual comparison is Sokoban: there are still lots of levels that humans can beat that all Sokoban AIs cannot, including the AIs that came out of Deepmind and Google. The problem is that the training set is so much smaller, and the success heuristics so much more exacting, that we can't get the same benefits from scale as we do with chess. Math is even harder than that.

(I wonder if there's something innate about "planning problems" that makes them hard for AI to do.)

[raincole]

> Unless mathematics is fundamentally more complicated than chess or go

"Fundamentally" carries the weight of the whole solar system here. Everyone knows mathematics is more conceptually and computationally complicated than chess.

But of course every person has different opinions on what makes two things "fundamentally" different so this is a tautology statement.