The Lumenary · Research pathways

AI-assisted mathematical research

Name: ______________________

Date: ______________________

You will learn to

Describe the ways AI systems assist mathematical research — literature search, code and experiments, search for constructions, conjecture generation, proof drafting, autoformalisation and formal proof search — and the generate-and-verify loop behind reliable use
Distinguish a checkable construction (a lower bound) from an optimality or universal claim, and verify a machine-found certificate exactly, in Python and in Lean with decide
Read an announcement of an AI-assisted result critically, separating what was announced, independently checked, formally verified and published, and checking novelty against the literature
Summarise the dated record of AI contributions from 2021 to 2026, keeping what is known separate from what is open
Use AI tools in your own research responsibly, with verification, disclosure and fair credit

1.
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?
2.
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.The model had located existing papers that already solved the problems; the site listed them as open because its maintainer did not know of those papers.
- B.The model produced ten new proofs, later confirmed by the site's maintainer.
- C.The model's proofs were all found to be wrong.
- D.Nothing of value happened: finding old papers is not a contribution.
3.
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.)
- A.Announced
- B.Lean-verified — for the formal statement in the file
- C.Independently checked
- D.Published
- E.The open lemma is solved
4.
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)$ ?
5.
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?
- A. $S(4) \ge 35$ , and nothing more.
- B. $S(4) = 35$ .
- C. $S(4) = 35$ is likely, since the search tried many colourings.
- D. $S(4) \le 35$ , by the pigeonhole principle.
6.
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$ ?
- A.∃ c : ℕ → Fin 3, IsSchurColouring 13 c
- B.∀ c : ℕ → Fin 3, IsSchurColouring 13 c
- C.∃ c : ℕ → Fin 3, IsSchurColouring 14 c
- D.∀ c : ℕ → Fin 3, ¬ IsSchurColouring 14 c
7.
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.)
- A.That the formal statement, and every definition it uses, says what the problem says
- B.That #print axioms shows only propext, Classical.choice and Quot.sound
- C.That the file actually builds, with the stated Lean and Mathlib versions
- D.Every one of the 3,000 lines of the proof, by hand
- E.That two other AI systems agree the proof is correct
8.
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.
Computational — Practice
9.
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?
- A.Cite the 2019 paper for the related construction, state precisely in the paper how the AI system was used (which system, for what, and how its output was checked), and take responsibility for the whole paper as its authors.
- B.List the AI system as a co-author, since it had the key idea.
- C.Say nothing about the AI system, since you verified everything yourself.
- D.Do not cite the 2019 paper, since neither you nor the AI system used it consciously.

Answer key — AI-assisted mathematical research

1.
For $x = 1, \dots, 6$ the number of $y$ with $x \le y \le 13 - x$ is $14 - 2x$ : that is $12 + 10 + 8 + 6 + 4 + 2 = 42$ (for $x \ge 7$ there are none). Checking 42 triples takes microseconds, while finding a colouring that passes means searching among $3^{13} \approx 1.6$ million colourings. This asymmetry is what makes the generate-and-verify loop work.
2.
The model found published solutions to problems the database listed as open. Bloom called the original description a dramatic misrepresentation, and the most widely shared post was deleted. The lesson: "solved by AI" and "found in the literature by AI" are different claims, and both should be checked by reading the papers.
3.
The result is announced and Lean-verified for the formal statement in the file. It is not yet independently checked (nobody outside has read the statement or the proof) nor published. Whether "the lemma is solved" depends on the faithfulness of the formal statement — the step people must check.
4.
$S(2) \ge 4$ , $S(3) \ge 13$ , $S(4) \ge 40$ ; in general $S(k) \ge (3^k - 1)/2$ . The bounds for $k = 2, 3$ are sharp, but $S(4) = 44$ : computer-found colourings beat the general construction, and such small cases, amplified by product constructions, give better exponential lower bounds for $S(k)$ and for $R(3; k)$ .
5.
Only the lower bound $S(4) \ge 35$ follows: each colouring found is a certificate. An upper bound would require a proof covering all colourings — by argument or by a complete (and ideally certified) exhaustive search, as for $S(4) = 44$ (Baumert, 1965) and $S(5) = 160$ (Heule, 2017).
6.
$S(3) \ge 13$ means some 3-colouring of $\{1, \dots, 13\}$ is a Schur colouring: ∃ c : ℕ → Fin 3, IsSchurColouring 13 c, proved by the witness searchCertificate. The universal statement with 14 is the optimality claim $S(3) \le 13$ , which the lesson checks by exhaustive search in Python but does not formalise.
7.
Check the trusted base: the formal statement and its definitions (faithfulness), the axioms (#print axioms), and that the build is reproducible. The proof steps themselves are checked by the kernel. AI agreement adds nothing that the kernel does not already provide, and nothing about faithfulness.
8.
```
def is_schur(colouring):
    n = len(colouring) - 1
    for x in range(1, n + 1):
        for y in range(x, n + 1 - x):
            if colouring[x] == colouring[y] == colouring[x + y]:
                return False
    return True


def triple(colouring, k):
    m = len(colouring) - 1
    low = colouring[1:]
    return [0] + low + [k] * (m + 1) + low
```
Starting from $\{1\}$ the construction gives Schur colourings of $\{1, \dots, 4\}$ , $\{1, \dots, 13\}$ , $\{1, \dots, 40\}$ and $\{1, \dots, 121\}$ with 2, 3, 4 and 5 colours. The verifier is the trusted part: the tests would catch a wrong construction even if you were sure of your proof.
9.
Cite the earlier paper, disclose the AI use specifically, and take responsibility as the (human) authors. This mirrors the unit distance remarks, which credit the key ideas, in retrospect, to earlier work by Ellenberg–Venkatesh, Golod–Shafarevich and Hajir–Maire–Ramakrishna while describing exactly what the model did.