Project Reinnman · mathematics and research infrastructure
Building systems that know when a proof has not happened
Making AI-assisted mathematics more rigorous, reproducible, and honest.
Reinnman investigates Robin’s inequality, an established equivalent formulation of the Riemann Hypothesis, using exact colossally abundant number arithmetic, symbolic reduction, directed numerical methods and Lean formalization. Alongside the mathematics it builds the instruments: source locks, obligation graphs, claim ceilings, independent replay and adversarial mutation testing.
Project Reinnman has not proved the Riemann Hypothesis, and is not close to proving it.
The immediate goal is to produce mathematics and research infrastructure that are worth having at every level below that objective, while keeping verified theorems, conditional arguments, numerical evidence and open conjectures strictly apart.
What it has not produced
The list that usually goes last
A program about detecting when a proof has not happened cannot put its own negative results below its achievements. The Riemann Hypothesis remains open, and nothing here is offered as a step whose next step is a proof.
- A proof of the Riemann Hypothesis.
- A proof of Robin’s inequality.
- A new zero-free region.
- An unconditional prime-pair power saving.
- A complete Preissmann Lemma 6 formalization.
- External mathematical validation, peer review, or independent institutional replication.
- A publication-ready replacement for the withdrawn legacy paper.
The decisive unconditional asymptotic inequality is not proved. What remains is explicit: one exact unified carrier holding all endpoint, nonlinear, cutoff and state-dependent support terms; an exact transform for it; a genuinely new unconditional positive lower bound; an explicit asymptotic threshold; and a gap-free finite certificate below that threshold. No finite computation, formal interface, conditional estimate or sampled numerical pattern stands in for any of those.
What it has produced
Each result at the height it was actually established
The label on each item is its evidence ceiling, and it is the point rather than a decoration. A Lean file that compiles proves what its hypotheses allow and nothing more, so formal compilation is never reported as evidence that an uninstantiated hypothesis holds.
- computationalAn exact arithmetic engine for colossally abundant numbers, with an independently reconstructed finite computation path and frozen evaluation endpoints.
- paper proofAn exact four-way decomposition of the Robin gap into cutoff, higher-stratum, Euler-product and Mertens components.
- machine-checkedLean components for finite spectral identities, endpoint bookkeeping, Preissmann-style inequalities and exact rational certificate checking.
- paper proofA positive Laplace-mixture proof of the formula-(5) E2 deformation, and a corrected separation of the original sequence from its affine replacement.
- paper proofExact no-go results ruling out classes of method that cannot close the estimate without more arithmetic information, including diagonal relaxations, fixed finite wavelets and norm-only large-sieve bounds.
- conditionalThe strongest formal packages remain conditional on open analytic receipts, and formal compilation is not treated as evidence that an uninstantiated hypothesis has been proved.
- prototype, unevaluatedA Proof Observatory: a provenance-first research environment with claim ledgers, obligation graphs, source locks and adversarial mutation testing.
- prototype, unevaluatedA benchmark of genuine mathematical defects taken from this project’s own failures, with blinded prompts and sealed adjudication keys.
Withdrawn
Claims this project retired, in writing
A central spectral interpretation in the original manuscript was wrong. Finding it changed the direction of the project and produced the controls that the rest of this page describes. The affected claims were withdrawn rather than quietly dropped, and they stay here so the corrections and their dependencies can be audited by someone who was not present.
- A proposed “double spectral hit” identity, and the Quasi-RH threshold that depended on it.
- Conclusions resting on inadmissible zero perturbations.
- An incorrect spectral orientation carried from the original manuscript.
- A false finite-prefix equidistance inference, and an unsafe special-function branch that generated a false negative witness.
The ability to detect and retire an attractive but incorrect result is one of the project’s real outputs. It is also where the benchmark comes from.
The Proof Observatory
A benchmark made of this project’s own mistakes
AI systems produce mathematical argument quickly, and evaluation of them tends to ask whether the final answer is right or whether a proof assistant accepted it. Neither question catches a hidden premise, a restatement of the original problem wearing new notation, a finite check promoted to an infinite theorem, or a valid subresult thrown away with the broken proof around it.
So the defects found here were turned into evaluation tasks. Each asks whether a mathematician or a model can find the decisive defect, tell a broken proof from a broken theorem statement, keep the parts that survive, propose the minimal repair, and state an accurate ceiling for what is left.
- Hidden analytic premises
- Invalid limit interchange
- Indexing and endpoint errors
- Source mismatch
- Branch discontinuity
- Target-equivalent restatement
- Circularity
- Numerical evidence promoted to theorem
- Stale dependencies
- Claim-ceiling inflation
The Observatory has not had an external pilot. There are no external reviewer outcomes, no efficacy estimate, no public adoption and no independent institutional replication. Those are the missing evidence events, not an oversight in the description.
Transparency
Project Reinnman has not proved the Riemann Hypothesis. Computational experiments, conditional arguments, paper-level analytic reasoning and formally verified theorems are labelled separately throughout. Withdrawn claims remain visible so corrections and dependencies can be audited. Its theorem claims and computational results have not received comprehensive external peer review.
The next objective is not another wave of experiments. It is to freeze one exact theorem object, put it in front of independent reviewers, and find out whether these assurance methods measurably improve mathematical reliability. A null result there would be worth having too: it would say which controls cost more than they return.
The project entry sits with the rest of the portfolio, and the research page carries the verification work this grew out of.