The Repository Was Green. RH Was Still Open.

The repository kept getting greener, and that made me nervous. Green is usually good news; here it could also make a reader believe something we had not done.

More definitions compiled. More Lean files contained checked proofs. More supporting stages could truthfully be marked complete. Numerical experiments accumulated. Conditional bridges became precise enough to formalize.

The central theorem was still open.

There is one sentence this project must never accidentally imply:

We proved the Riemann Hypothesis.

Avoiding that sentence in the README is easy. Avoiding it across a growing research system is harder.

A reader sees thousands of lines of formal mathematics and a dashboard full of completed components. An API exposes a type named after the target theorem. A generated status page says “complete” beside several stages. A placeholder proof is accepted during development. No individual line says the impossible thing, but the repository’s overall shape begins to suggest it.

The F₁ research repository takes a stricter approach: identify the missing mathematical object, prove the surrounding machinery, preserve empirical evidence, and encode the unresolved crux as unresolved.

The open theorem becomes a boundary the software can see. That is a useful result even when the theorem remains stubbornly open.

“Work on RH” is not a sufficiently precise plan

A famous theorem is too large to serve as an implementation target by itself.

A research architecture needs to say which construction or implication is actually missing.

One geometric route compares the number-field case with the function-field case. Over a function field, Frobenius acts on cohomology, and an intersection-positivity result constrains the relevant eigenvalues. The number-field analogy seeks a corresponding geometric and cohomological object around Spec ℤ over 𝔽₁.

The repository frames the missing center as a two-dimensional arithmetic square with an intersection theory strong enough to provide the required Hodge-index-style positivity.

flowchart TD
    FF[Function-field theorem] --> M[Known geometric mechanism]
    M --> A[Number-field analogy]
    A --> S[Arithmetic square over F1]
    S --> I[Intersection pairing]
    I --> H[Hodge-index-style positivity]
    H --> RH[Riemann Hypothesis]

    S -. construction incomplete / contested .-> O[Open boundary]
    I -. required theorem .-> O
    H -. crux .-> O

That diagram is useful because it lets the repository ask concrete questions instead of gesturing toward a famous result:

• Has the proposed square been constructed?
• Does it satisfy the required universal property?
• Is the intersection pairing defined on the right objects?
• Has the needed positivity theorem been proved?
• Is the implication from those assumptions to RH formalized?

Every missing item can become a typed obligation with a status.

The phrase “toward RH” then has a technical meaning rather than functioning as a halo around unrelated mathematics.

A large amount of evidence can remain finite

Li’s criterion gives a clean example of the boundary between evidence and the theorem.

The Riemann Hypothesis is equivalent to positivity of an infinite sequence:

$$\mathrm{RH} \iff \lambda_n > 0 \quad \text{for every } n \ge 1$$

Proving $\lambda_1 > 0$ is true mathematics. Proving $\lambda_2 > 0$ adds more. Checking the first million coefficients numerically may be substantial evidence.

None of those statements inhabits the universal claim:

$$\forall n \ge 1,\ \lambda_n > 0$$

flowchart LR
    L1[Proof: lambda_1 > 0] --> E[Finite evidence]
    L2[Proof: lambda_2 > 0] --> E
    LN[Checked lambda_n for n <= N] --> E
    E -. does not imply .-> U[Universal positivity]
    U --> RH[RH via Li criterion]

This is where types can protect the research record.

A function that checks a finite prefix should return a finite-check result. A proof of one coefficient should not be coercible into universal positivity. A numerical witness should not inhabit the same type as a kernel-checked theorem.

The difference is obvious when written in a paragraph. The type boundary keeps it obvious after years of refactoring, automation, and generated reporting.

“Open” should be represented, not inferred

Research repositories often use status words such as established, partial, conjectural, open, refuted, and superseded.

If those words live only in prose, they drift.

The central result can instead be modeled as an absent proof:

struct ResearchStatus<P> {
    evidence: Vec<EvidenceRecord>,
    proof: Option<P>,
}

When the crux remains open, proof is None.

Not a fake inhabitant. Not a boolean inferred from the number of passing examples. Not an unchecked axiom hidden behind a friendly API.

stateDiagram-v2
    [*] --> Open
    Open --> Partial: supporting theorem established
    Partial --> Open: proposed bridge refuted
    Partial --> Established: full proof term supplied
    Open --> Established: full proof term supplied
    Established --> [*]

The only transition to Established should require the artifact that the word claims exists.

A generated report can then say all of the following at once:

• a constructive analytic component is implemented
• particular coefficients have checked positivity proofs
• the conditional bridge is formalized
• the universal positivity proof is absent
• the Riemann Hypothesis remains open

That is more informative than one green project badge, and much harder to misread.

A placeholder is useful until it starts publishing confidence

Lean’s sorry is valuable while a theorem is being sketched. It lets the surrounding design elaborate before every proof is complete.

The danger begins when the public status treats a file as proved merely because Lean accepted it with a placeholder.

An honest repository can use several boundaries:

1. keep conjectural statements in an explicitly named namespace
2. represent missing proofs as data rather than theorem values
3. make CI reject sorry in established modules
4. distinguish interface assumptions from proved results
5. generate status from the proof dependency graph

flowchart TD
    T[Target statement] --> Q{Proof term exists?}
    Q -- yes --> K[Kernel checks term]
    K --> E[Established theorem]
    Q -- no --> O[Open / conjectural record]
    O --> R[Research dependency remains visible]

The project can still build useful code around an assumption. What it cannot do is allow the assumption to cross into the established layer without an explicit transition.

I do not want sorry to become project management: a placeholder silently standing in for “we plan to solve this eventually” while every downstream dashboard behaves as though the theorem already exists.

Formalize what would be sufficient

An open construction often has a known shape even when the object itself has not been built.

The function-field case may tell us which structures and theorems a number-field analogue would need. Formalizing that mechanism is valuable because it replaces vague sufficiency arguments with explicit assumptions.

flowchart LR
    A[Abstract assumptions] --> M[Formal mechanism]
    M --> C[Conditional conclusion]

    X[Proposed arithmetic object] --> V{Satisfies assumptions?}
    V -- proven --> C
    V -- not proven --> O[Open obligation]

The repository can prove:

• which input assumptions are required
• what kind of intersection pairing is sufficient
• the exact positivity statement needed
• how that statement implies the desired spectral conclusion
• which assumption remains unavailable

A conditional theorem is not the final solution. It still reduces ambiguity.

The next contributor no longer has to debate informally whether “some geometric positivity” might be enough. The proof assistant can display the exact hole the candidate construction must fill.

Supporting mathematics should be proud of its actual range

Work near an open theorem requires substantial infrastructure: exact rational arithmetic, constructive real and complex numbers, convergence, transcendental functions, zeta functions in proved regions, arithmetic identities, algebraic machinery, tactics, and normalizers.

Each component can be real, reusable, and formally established.

The temptation is to let proximity to the target inflate what each piece means.

The repository has to keep distinctions such as these explicit:

• constructing $\zeta(s)$ where a series converges is not analytic continuation to the critical strip
• implementing a constructive approximation to $\Gamma$ is not every identity required later
• proving finitely many Li coefficients is not universal Li positivity
• defining a candidate square is not proving its universal property
• proving that property is not proving the Hodge index theorem

flowchart TD
    R[Constructive reals] --> C[Constructive complex numbers]
    C --> Z[Zeta in proved domain]
    Z --> L[Finite Li coefficients]
    L --> E[Evidence]

    E -. gap remains .-> U[Universal Li positivity]
    U --> RH[Riemann Hypothesis]

Saying where a theorem stops does not diminish the work. It makes the work reusable outside the original ambition.

A library component with a precise domain can be trusted by another project. A component whose documentation borrows confidence from an open theorem cannot.

“Complete” needs a local subject

The word complete is especially dangerous in staged research.

“Stage B complete” may truthfully mean that every implementation task defined for Stage B has landed. A reader can easily hear “the mathematical program is complete.”

A more useful status names its axis:

implementation: complete
verification: partial
research claim: open

Or, in prose:

Stage B implementation checklist complete; central theorem remains open.

This is the same separation I want in systems projects. Code can exist while external conformance remains incomplete. Tests can pass while a performance budget is unmet. A mechanism can work while a product hypothesis remains unsupported.

One green word should not be forced to carry all of those meanings.

Counterexamples belong beside the proofs

A long research program becomes stronger when it preserves the constructions that fail.

A counterexample may show that a proposed positivity statement is too weak, a spectrum map loses information, a candidate product collapses dimension, a finite condition cannot control the universal case, or an experimental check is vacuous.

flowchart LR
    P[Proposed lemma] --> T[Formal test / model]
    T --> C[Counterexample]
    C --> R[Refine statement]
    R --> N[New proof obligation]

Deleting the failed candidate throws away the boundary it discovered.

The counterexample often survives changes in the implementation better than the failed code does. It tells future work which attractive shortcuts have already been ruled out and why.

That is part of the proof architecture, not an embarrassing appendix.

Readers need a map of confidence

A repository near a famous open problem attracts readers with very different mathematical backgrounds. The project should make it easy to distinguish:

• kernel-checked proofs
• conditional theorems
• numerical or empirical evidence
• candidate constructions
• refuted directions
• the central open obligations

flowchart TB
    P[Proved] --> D[Public status page]
    C[Conditional] --> D
    E[Empirical evidence] --> D
    O[Open] --> D
    R[Refuted] --> D
    D --> Reader[Reader sees exact boundary]

That status page is not an apology. It is navigation.

The larger the ambition, the more important it becomes to show where confidence comes from. Otherwise a reader has to inspect every theorem dependency and experimental artifact just to learn what the project itself believes.

The honesty boundary should be mechanical

The strongest form of careful wording is not wording at all. It is a repository that rejects dishonest states.

CI can enforce that:

• established theorem modules contain no placeholders
• open claims cannot be exported as proved values
• finite checks cannot inhabit universal proof types
• generated documentation reads the same status ledger as the code
• dependency graphs expose assumptions
• refuted directions are not enabled as defaults
• every public status points to a source artifact

This does not prove the Riemann Hypothesis.

It proves that the repository knows it has not proved it.

That is an important property for an ambitious project to maintain as the surrounding work becomes more impressive.

Open problems still produce real software

There is a false choice between closing the famous theorem and producing nothing of value.

A careful program can create verified mathematical libraries, better formulations of the missing construction, reusable conditional mechanisms, counterexamples, computational evidence, proof tooling, and a durable map of unresolved obligations.

Those artifacts remain worthwhile even if the central theorem stays open.

Mark the missing object

For an ambitious mathematical project, write down the one object that would close the central gap:

• what type should it have?
• which assumptions would it consume?
• which theorem would it make available?
• what would count as a real proof term?
• which nearby results are useful without being that object?

Put that missing object next to the green work. Readers should not have to infer the boundary from the amount of code.

The repository getting greener should be a sign that more of the surrounding mathematics is understood—not a visual trick that causes the open center to disappear.

That is the operating rule I want F₁ to preserve:

Build the machinery. State exactly what it proves. Name the object that is still missing. Keep the crux open until a real proof term closes it. A green repository is not permission to skip that last sentence.