Answers.Body: <p>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 <em>transfinite</em> induction and <em>non-constructive</em> proofs with <em>choice</em> function typical in ZFC set theory and halting problem like <em>undecidable</em> propositions.</p>
  <p>There are proof assistants like Coq or Lean which allow mathematicians to construct and verify proofs with the <em>assistance</em> of AI but still require significant input from the user in terms of guidance and formulation without guaranteed automated theorem proving result.</p>
  <p>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.</p>
  <p>Lample et al. (2021). <a href="https://arxiv.org/abs/1912.01412" rel="nofollow noreferrer"><em>&quot;Deep Learning for Symbolic Mathematics&quot;</em></a>.</p>
  <blockquote>
  <p>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.</p>
  </blockquote>
  <blockquote>
  <p>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.</p>
  </blockquote>
  <p>Polu et al. (2022). <a href="https://arxiv.org/abs/2202.01344" rel="nofollow noreferrer"><em>&quot;Formal Mathematics Statement Curriculum Learning&quot;</em></a>.</p>
  <blockquote>
  <p>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.</p>
  </blockquote>
  <p>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.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2024-08-08T08:46:40.203Z
Answers.LastActivityDate: 2024-08-08T08:46:40.203Z
Answers.UserDisplayName: cinch
Body: <p>Recently, Google Deepmind made news by presenting AlphaProof, <a href="https://www.technologyreview.com/2024/07/30/1095467/how-machines-that-can-solve-complex-math-problems-might-usher-in-more-powerful-ai/" rel="nofollow noreferrer">solving Math Olympiad problems</a>. Apparently, AlphaProof is weaker in combinatorics (I couldn't find the source.</p>
  <p>How about elementary problems in infinitary combinatorics such as this?</p>
  <blockquote>
  <p>Is there a bijection <span class="math-container">$f:\newcommand{\N}{\mathbb{N}}\N\to\N$</span> such that <span class="math-container">$f(S)\neq S$</span> whenever <span class="math-container">$S\subseteq \N$</span> is infinite and <span class="math-container">$\N\setminus S$</span> is infinite?</p>
  </blockquote>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2024-08-06T11:14:24.880Z
Comments.Text: Your question is a bit vague. Please, ask a more specific question.
Comments.UserDisplayName: nbro
Tags: <math><deepmind>
Title: AlphaProof and infinitary combinatorics
UserDisplayName: Dominic van der Zypen
ThreadText: # AlphaProof and infinitary combinatorics
  
  (Asked by: username_0 on 2024-08-06)
  
  Recently, Google Deepmind made news by presenting AlphaProof, [solving Math Olympiad problems](https://www.technologyreview.com/2024/07/30/1095467/how-machines-that-can-solve-complex-math-problems-might-usher-in-more-powerful-ai/). 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?
  
  **Tags:** math, deepmind
  > **Comments:**
  > **username_1**: Your question is a bit vague. Please, ask a more specific question.  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_2 on 2024-08-08. Score: 4 | Accepted answer
  
  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"*](https://arxiv.org/abs/1912.01412).
  
  > 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"*](https://arxiv.org/abs/2202.01344).
  
  > 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.
  
  
  ---
  
  