Submit a problem

What to submit

A single, precise statement from one of the domains below. The best candidates are results you can point to in a textbook or paper: the machine is very good at careful transcription and patchy at genuinely new mathematics. Your own conjectures are welcome; expect some of them to end up under needs help. Famous open problems are out of scope.

• Theoretical Computer Science — The mathematics of computation: what can be computed, at what cost, and with what guarantees. Machine models, complexity classes, algorithm analysis, and the…
• Optimization & Operations Research — The theory of optimizing over structured sets: when an optimum exists, when it is certified by a dual object, and how fast an iterative method reaches it.
• Probability & Mathematical Statistics — Measure-theoretic probability and the theory of statistical inference: limit behaviour, concentration, what an estimator can achieve, and what no estimator can.
• Mathematical Logic & Foundations — The mathematics of formal systems themselves: what structures satisfy a theory, what a proof system can and cannot prove, and the set-theoretic ground…
• Game Theory & Mathematical Economics — Strategic interaction and the theory of collective decisions: when equilibria exist, what aggregation rules are possible, and what mechanisms can be made…
• Theoretical Physics — The mathematical structure of physical theory: the variational principles that generate the equations of motion, the symmetries that constrain them, the…

Write the statement the way you would in a paper. LaTeX between $…$ is rendered. If you know Lean, you may add a Lean statement, but you do not have to.

What happens next

1. Review. A maintainer reads every submission before the machine spends anything on it, since every attempt costs tokens. Accepted problems get the accepted label; declined ones are closed with a reason. Until then a submission is only counted on this site, not shown.
2. Formalization. The machine writes its own Lean statement. It must type-check, pass the round trip against your English, and not reuse a name for something it is not. Any Lean you supplied is reference text and is never run as-is.
3. Proof. The prover works on it like any other node. If it gets stuck it splits the statement into lemmas, and the problem shows as needs help, with the exact statement it is stuck on.
4. Publication. When everything answering your problem is proved, it appears under Problems and in the knowledgebase, with its full proof, and the issue is updated.

Credit

Your GitHub handle is shown on the problem as the person who posed it. Everything the machine produces is public and free to use; by submitting, you agree that your statement may be published, reformulated and built on by anyone.

Challenging a result

Whether a proof is correct is not up for debate: it elaborates and #print axioms is clean, or it is not on this site. Everything else is. If a declaration's name claims more than it proves, if a statement is trivial or vacuous, or if a definition is not the one the subject uses, open a challenge. Every declaration page has a button for it too.

Just want to talk?

Questions, ideas for the curriculum and results you built on top of the knowledgebase belong in the discussions.