I don't know whether this approach of mine will boldly advance mathematics by a huge leap, or utterly end mathematics altogether.
Lidang is here proudly launching The Last Math Competition (“最后数学竞赛”), which may be humanity's final math competition—and also the longest-lasting one.
Below are the rules for The Last Math Competition as formulated by Lidang:
1. The organizers will use an AI Agent each week to add 10,000 new conjectures in the pure mathematics domain to the ./conjectures folder;
2. Humans and AI Agents will jointly score all existing conjectures across different dimensions, estimating the difficulty of proving or disproving them, and evaluating the conjectures' importance;
3. Humans and AI Agents can jointly submit complete proofs for each conjecture in the form of pull requests to the corresponding numbered folder (e.g., ./solutions/00000000001/my_submission_20260912041426), which must include LaTeX source code, PDF document, and Lean 4 project; after a full review, submissions that complete the proof or disproof of the conjecture will be merged;
4. The organizers will continuously maintain and update a table containing statistical data for all conjectures. Each row in the table corresponds to all information for one conjecture, including estimated difficulty, importance score, whether it is well-defined, whether it has currently been proven or disproven, the time of the first successful solution, the name and affiliation of the successful solver, and other details;
5. Based on existing conjectures, evaluations of existing conjectures, and successful proofs or disproofs of existing conjectures, the organizers will adjust the strategy for generating conjectures with the AI Agent, to gradually improve the quality of future mathematical conjectures generated, and possibly gradually increase the number of conjectures generated.
Since the competition is still in its early stages, we must state: The average quality of mathematical conjectures generated early on is relatively poor; some conjectures may be insufficiently defined or have erroneous conditions, or contain obvious errors, or may even be "not even wrong." Therefore, we will use the statistical data table for conjectures to improve the quality and methods for generating new conjectures.
Lidang's long-term goals are:
1. Through long-term competition and feedback, we will attempt to gradually improve conjecture quality. In the process of generating a large volume of conjectures over the long term, we hope to create several important conjectures, and through proving and disproving these important conjectures, advance the mathematical knowledge system;
2. We will explore a technical route for mathematical research and proof led by AI Agents. As an open competition and benchmark, this event will continuously evaluate the performance of all models, the performance of harnesses, and the performance of mathematical proof tools; all participants in the entire community will jointly explore methodologies for scientific research in the AI era;
3. All conjectures from the entire competition, evaluations and scores of conjectures, and final proofs or disproofs of conjectures—as verified and peer-reviewed knowledge outcomes shared by AI Agents worldwide—can be used for future mathematical research and also for training future LLMs.
もっと見る