Polymath

Make mathematical research easier to check, reproduce, and hand to the next reviewer.

Polymath is a Rust CLI that checks a finite mathematical certificate, records bounded verification runs, retrieves research notes, and compares the scope of different claims. It keeps the artifact, its assumptions, and the evidence together.

The included example covers 4,075 candidate integers from Tao's tenth discriminant challenge. A successful check establishes that every candidate has a valid finite witness. The broader number theory argument remains a separate responsibility.

Try it

You need Rust and Cargo. Clone the repository, then run the commands below from its root. Cargo may download dependencies on the first build; the CLI makes no AI provider calls.

git clone https://github.com/ruvnet/Polymath.git
cd Polymath

Start with the read only demo:

cargo run --locked --release -- demo

Check the example directly:

cargo run --locked --release -- verify examples/tao-32768.certificate.json

Record a verification run and inspect its journal:

cargo run --locked --release -- run --id example-001 --certificate examples/tao-32768.certificate.json --state .polymath
cargo run --locked --release -- status --state .polymath

Find related notes and compare claims:

cargo run --locked --release -- recall examples/research-notes.json --query 'determinant valuation' --limit 3
cargo run --locked --release -- compare examples/claims.json

The run command creates local state and permits at most four started verifications per journal. Repeating a completed ID with the same certificate, expected bounds, and executable returns the saved receipt. A changed request under that ID is rejected and stops the journal. An interrupted or failed run blocks new work for inspection.

The other commands above inspect inputs without starting an optimizer. This local allowance does not reset, resume, or spend any earlier Tao numerical research allowance. To persistently stop a local journal, use cargo run --locked --release -- stop --state .polymath; there is no automatic reset command.

What a passing check means

The example examines integers satisfying 163 < q < 32768 and q ≡ 3 mod 8. It verifies complete coverage and the arithmetic witnesses in the certificate. The file is 6,486 bytes and contains 4,075 candidates.

Three mathematical inputs remain outside that finite check:

1. The analytic argument reduces the problem to q < 32768.
2. Any hypothetical remaining fundamental discriminant of class number one lies in the stated residue class.
3. The stated small noninert prime obstruction rules out class number one.

Evidence	What it establishes
Exact certificate check	Every candidate in the specified finite domain has a valid witness.
Journal receipt	A particular local action and artifact were recorded with their result.
Separate mathematical review	A reviewer has examined the general argument and its assumptions. The CLI does not supply that review.
Formal proof	A proof assistant accepts a precisely encoded theorem and its dependencies. Lean is not implemented here.

A journal receipt, a policy decision, or an admission check does not turn finite evidence into a general theorem. The example explicitly retains global_proof_verified: false.

Research notes

The v5 norm estimate note derives a refinement from 41 to 26 in one derivative error bound and proves the two required error thresholds using elementary rational estimates. It concerns the inherited interval from 2000 to 4000. It establishes no smaller discriminant cutoff.

The review statement records separate Codex agent checks, including a second route to the threshold inequalities. This is AI assisted written mathematics, with no human peer review or Lean verification claimed.

What is connected

Component	Current role	Boundary
Rust exact verifier	Checks the included finite obstruction certificate.	No analytic cutoff proof or general theorem checker.
Local journal	Records bounded verification actions and their results.	Local evidence; no independent attestation.
rGi	demo and run call the pinned policy evaluator for certificate verification.	A policy kernel, not an autonomous runtime or independent mathematics checker.
RuVector	Uses an in memory HNSW index to retrieve research notes.	Approximate lexical similarity from hashed tokens, not semantic embeddings or proof confidence.
Autogenous	demo and run call pinned upstream mutation admission code after exact verification.	Checks declared metadata structure, not certificate contents; no fitness judgement, signed promotion, or rollback execution.
Ruflo	Can coordinate the surrounding research project.	No Ruflo agent runtime is embedded in this CLI.
ruOS	Can provide an existing environment in which to run the CLI.	This repository does not provision or remotely control a host.
Metaharness	A future adapter for proposing and evaluating bounded experiments.	The earlier search loop has not been ported into this Rust CLI.

There is no autonomous AI provider runtime, automatic mathematical discovery, or paid compute provisioning in this release. The animated diagram describes the research workflow; separate review remains work for a reviewer.

Use it for a research contribution

Start with one claim whose inputs and acceptance condition can be written down. Keep its proposed artifact separate from the checker. Record the source version and assumptions, run the exact check, and give the artifact and receipt to a separate reviewer.

Compare claims by their conclusions, assumptions, checked ranges, and review status. A smaller cutoff, a shorter certificate, and a faster verification are different results. The compare command helps keep those distinctions visible; it does not rank mathematical truth.

The main remaining uncertainty in the example is the general analytic dependency chain. Improving the certificate or its journal does not resolve it. The useful next step is a separate review of one named mathematical obligation.

Provenance

The example grew out of work on Terence Tao's tenth discriminant challenge. Its finite domain follows the elementary companion in twinheterodox/tenth-discriminant. The certificate was generated in that research workflow; it is not a new analytic bound.

The upstream papers and challenge contributions retain their own authorship and review status. We link to them rather than redistribute their papers. This repository makes no claim to a challenge record, a new theorem, or priority for their mathematical ideas. The fixture provenance records its exact hash, source, and scope; third party notices identify the upstream software.

Architecture and trust boundaries · Architecture decision · Contributing

Acceptance check: cargo test --locked --all-targets followed by cargo run --locked --release -- demo must pass while the finite example continues to report that the global proof is unverified.