AI-assisted mathematical research

To verify a proposed Schur colouring of $\{1, \dots, 13\}$, a checker examines every triple $(x, y, x + y)$ with $1 \le x \le y$ and $x + y \le 13$. How many triples is that?

In October 2025 posts by OpenAI researchers said that GPT-5 had found solutions to ten Erdős problems listed as open on erdosproblems.com. Which description of what happened is accurate?

A company's blog post says its model proved an open lemma. It links a Lean file that compiles with no sorry, and a PDF of the informal proof written with the model's help. No one outside the company has commented yet. Using the lesson's labels, which descriptions are accurate? (Choose all that apply.)

Schur's tripling construction gives $S(k + 1) \ge 3 S(k) + 1$. Starting from $S(1) = 1$, what lower bound does it give for $S(4)$?

A randomised local search finds verified Schur 4-colourings of $\{1, \dots, n\}$ for every $n \le 35$, and none for $n = 36$ within its budget. Which conclusion is justified?

Using the lesson's definition IsSchurColouring n c (no colour class of c on {1, …, n} contains x, y, x + y), which Lean statement expresses the lower bound $S(3) \ge 13$?

An AI system returns a 3,000-line Lean proof of an open problem whose statement it also formalised. Before you believe that the problem is solved, which of the following must you check? (Choose all that apply.)

Write a verifier is_schur(colouring) (where colouring[x] is the colour of x for 1 <= x <= n and colouring[0] is unused), and Schur's construction triple(colouring, k), which turns a Schur colouring of {1, ..., m} with colours 0, ..., k - 1 into one of {1, ..., 3m + 1} with colours 0, ..., k. The tests apply triple four times starting from [0, 0] (the colouring of {1}) and check every result with your verifier.

Working on a paper, you asked an AI system for ideas; it suggested the key construction, which you then checked in detail, generalised and proved correct yourself. It later turned out that a 2019 paper contains a closely related construction. What is the appropriate way to handle credit?