Maith is a research workspace for using AI to explore open mathematics—without confusing plausible text, numerical evidence, or symbolic output with proof.
Mathematics with AI should be ambitious and auditable. Open problems demand more than pattern matching: precise definitions, awareness of known obstructions, novel ideas, and arguments that withstand independent checking. Maith organises major problems as detailed dossiers and provides a disciplined workflow for exploring them with AI, computer algebra, formal tools, and human mathematical judgment.
Our standard: AI can accelerate discovery; proof must remain explicit, reproducible, and independently verifiable.
AI may generate ideas; mathematics requires independently checkable proof.
An AI answer can be useful when it proposes a lemma, finds a counterexample to an overstrong claim, suggests a computation, translates notation, or maps an argument's dependencies. It is not evidence that an open problem has been solved merely because it sounds coherent or produces many correct local steps.
| Task | Useful AI role | Required human or tool check |
|---|---|---|
| Learn a problem | Explain definitions at several levels and suggest prerequisites | Compare with standard references |
| Explore examples | Generate small cases, invariants, and candidate constructions | Use exact code and validate every output |
| Find failure modes | Search for missing cases, hidden assumptions, and counterexamples | Verify the counterexample or gap directly |
| Design experiments | Propose a CAS, numerical, or combinatorial search | Make the code public and reproduce it independently |
| Develop a proof | Organise lemmas and identify applicable theorems | Prove every lemma and check each hypothesis |
| Formalise a result | Translate a proof plan into Lean, Coq, or another proof assistant | Require the proof assistant to accept the final theorem |
- A fluent derivation may contain a subtle false equality, a lost quantifier, or an unjustified interchange of limits.
- A symbolic-algebra transcript is only reproducible evidence if the exact executable source, inputs, version information, and output are available.
- Numerical verification over a large range never proves an unbounded claim without a rigorous reduction to that finite range.
- A claim that overturns a well-known open problem needs extraordinary transparency: an explicit proof, independent expert review, and reproducible computation where computation is used.
Choose a dossier from PROBLEM.md. Rewrite the claim using explicit quantifiers, domains, and definitions. Ask AI to identify ambiguous terms, but confirm the standard formulation from reliable mathematical sources.
List every theorem, definition, and lemma your approach needs. For each theorem, record its exact hypotheses. AI can produce a useful first map; it must then be checked against the literature or a formal library.
Before trying to prove a proposed identity or lemma, search for counterexamples with exact arithmetic. Small counterexamples are disproportionately valuable: they prevent weeks of work on a false generalisation.
Keep an explicit distinction between:
- observation — a pattern in examples;
- conjecture — a proposed universal statement;
- lemma — a statement with a complete proof;
- theorem — a result whose dependencies have all been verified.
AI is often strongest in the first two categories. The transition to the last two must be documented line by line.
For a computer-algebra or search result, include:
- the exact source file;
- the original formulas or input data;
- the command that runs it;
- package and language versions;
- exact output and assertions;
- an integrity hash; and
- ideally, an independent implementation or external rerun.
The Jacobian Conjecture project is the working
example in this repository of this standard: it includes report.py, an exact
symbolic verifier, and a technical report describing the calculation.
Ask a second AI, a CAS, a proof assistant, or a human reviewer to attack the argument rather than polish it. Productive review questions include:
- Which assumption was used without being stated?
- Does the argument cover all cases, including boundary and degenerate cases?
- Is a cited theorem being applied within its actual hypotheses?
- Can an exact computation independently reproduce the claimed identity?
- Does a claimed inverse, factorisation, or elimination really work globally?
The problem index contains detailed dossiers across number theory, arithmetic geometry, computation, geometry, combinatorics, analysis, and physics.
| Area | Examples |
|---|---|
| Number theory | Riemann Hypothesis · abc · Goldbach · Twin Primes |
| Arithmetic geometry | Birch and Swinnerton-Dyer · Hodge · Jacobian |
| Complexity | P versus NP |
| Analysis and physics | Navier--Stokes · Yang--Mills |
| Combinatorics and geometry | Hadwiger · Lonely Runner · Perfect Cuboid |
Every dossier is intended to answer: what the problem says, why it matters, what has been proved, what blocks current approaches, and how an AI-assisted investigation can be made rigorous.
Create a directory for the problem and include:
PROBLEM.md # precise statement, status, known results, obstacles
IDEAS.md # clearly labelled conjectures and exploratory notes
experiments/ # exact, executable searches or CAS checks
proof/ # lemma-by-lemma argument, with references and assumptions
REPRODUCE.md # commands, versions, output, and hashes
Use IDEAS.md to preserve speculative work. Do not place an unproved argument
in proof/, and do not label a result “solved” until it has a complete proof
or a formally checked derivation.
Maith does not exist to declare that AI has solved famous problems. It exists to make mathematical research more systematic: faster counterexample search, clearer proof obligations, better experiment design, and more reproducible collaboration between people and machines.