Recently, Google Deepmind made news by presenting AlphaProof, solving Math Olympiad problems. Apparently, AlphaProof is weaker in combinatorics (I couldn't find the source.
How about elementary problems in infinitary combinatorics such as this?
Is there a bijection $f:\newcommand{\N}{\mathbb{N}}\N\to\N$ such that $f(S)\neq S$ whenever $S\subseteq \N$ is infinite and $\N\setminus S$ is infinite?
Infinitary combinatorics often specifically deals with infinite sets, their properties and various types of functions defined on them, usually requiring a strong understanding of set theory and cardinality. As of now, state-of-the-art (SOTA) AI models like AlphaProof or theorem-proving tools based on AI have shown great potential in handling certain kinds of mathematical problems, especially in finite combinatorics, algebra, and even some areas of analysis. However, they still struggle with highly abstract or deeply infinitary problems, especially those requiring transfinite induction and non-constructive proofs with choice function typical in ZFC set theory and halting problem like undecidable propositions.
There are proof assistants like Coq or Lean which allow mathematicians to construct and verify proofs with the assistance of AI but still require significant input from the user in terms of guidance and formulation without guaranteed automated theorem proving result.
There're very few literature about deep learning's application to symbolic math compared to general NLP related multi-modal application area. I suggest first read below two recent papers.
Lample et al. (2021). "Deep Learning for Symbolic Mathematics".
In this paper, we consider mathematics, and particularly symbolic calculations, as a target for NLP models. More precisely, we use sequence-to-sequence models (seq2seq) on two problems of symbolic mathematics: function integration and ordinary differential equations (ODEs). Both are difficult, for trained humans and computer software... We propose an approach to generate arbitrarily large datasets of equations, with their associated solutions. We show that a simple transformer model trained on these datasets can perform extremely well both at computing function integrals, and solving differential equations, outperforming state-of-the-art mathematical frameworks like Matlab or Mathematica that rely on a large number of algorithms and heuristics, and a complex implementation (Risch, 1970). Results also show that the model is able to write identical expressions in very different ways.
These results are surprising given the difficulty of neural models to perform simpler tasks like integer addition or multiplication. However, proposed hypotheses are sometimes incorrect, and considering multiple beam hypotheses is often necessary to obtain a valid solution. The validity of a solution itself is not provided by the model, but by an external symbolic framework (Meurer et al., 2017). These results suggest that in the future, standard mathematical frameworks may benefit from integrating neural components in their solvers.
Polu et al. (2022). "Formal Mathematics Statement Curriculum Learning".
We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.
In summary AlphaProof leverages interleaved SOTA models of proof search and learning of a curriculum consisting of increasingly difficult problems, possibly along with some external system for further validation. Thus if your sample infinitary combinatorics problem is included in AlphaProof's training curriculum it's very likely it can find ways to solve it. However, for open problems or challenging tricky problems not in its training curriculum, AlphaProof would still have trouble to compete with competent human mathematicians.
