Assignment 1: Proof-Agent Natural-Language Proof

Course: AI for Mathematics (General Elective), Xiamen University Malaysia
Weight: 20%
Points: 100
Due: Friday, 29 May 2026, 23:59 Malaysia time
Submission: Email two files to hoxide@gmail.com
Email subject: [AI4Math XMUM GE] Assignment 1 - <Student Name> - <Student ID>

Task

Use an agentic coding assistant, such as Codex, Claude, opencode, or openclaw, to obtain, inspect, and launch a proof/proving agent. Rethlas is one good option, but students may use another suitable proof agent if they know how to use it. Choose an interesting mathematical problem that is precise enough for a complete proof, run the proof-agent workflow, and turn the resulting proof blueprint or proof artifact into a readable mathematical PDF.

The problem should be nontrivial but realistic for this assignment. Suitable examples include a theorem from combinatorics, graph theory, number theory, algebra, analysis, probability, optimization, or another mathematically rigorous area. The proof should be substantial: about 4-5 pages is expected, and a longer proof is welcome if the exposition remains clear.

Required Submission Files

blueprint.md: the proof blueprint or proof-search artifact for your problem. If your chosen tool uses another filename, export or rename the main proof artifact as blueprint.md.
A PDF file containing the polished mathematical proof.

Expected Workflow

Formulate a self-contained mathematical problem statement, including all definitions and hypotheses needed by a fresh solver.
Ask an agentic coding assistant, such as Codex, Claude, opencode, or openclaw, to obtain or identify a suitable proof/proving agent, inspect the local implementation or documentation, and determine the correct launch procedure.
Run the proof generation and verification or checking workflow supported by your chosen tool.
Inspect the generated blueprint or proof artifact and any verifier feedback. Repair the problem statement or proof if necessary.
Convert the accepted or final blueprint/proof artifact into a clean PDF proof written for a human mathematical reader.

What the PDF Should Contain

A clear statement of the theorem being proved.
Definitions, notation, and assumptions used in the proof.
A complete proof, not only a proof sketch.

Students should email exactly the two required files, blueprint.md and their proof PDF, to hoxide@gmail.com.