How to Build Around an Open Theorem Without Claiming It

There is one sentence this project must never accidentally say:

We proved the Riemann Hypothesis.

That sounds easy to avoid. It gets harder as a repository accumulates formal definitions, verified lemmas, constructive analysis, numerical evidence, and increasingly complete pieces around the open center.

A reader sees thousands of lines of Lean and a long list of established components. A generated status page says “complete” next to several stages. An API exposes a type named after the target theorem. Somewhere, a boolean defaults to true because the implementation needed a placeholder.

The project can overclaim without anyone writing the false sentence directly.

The F₁ research repository takes a useful approach: name the missing object precisely, build the surrounding mathematics, and encode the unresolved crux as unresolved.

The open theorem becomes a boundary the software can see.

Start by naming what is missing

“Work on the Riemann Hypothesis” is not an architecture.

A useful research program identifies the specific construction or implication that remains absent.

One geometric route compares the number-field case to 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 asks for 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

This is much better than surrounding the theorem with a cloud of suggestive code.

The repository can ask concrete questions:

• Is the proposed square constructed?
• Does it satisfy the required universal property?
• Is the intersection pairing defined?
• Is the positivity theorem proved?
• Which bridge from that theorem to RH is formalized?

Each missing item can have a type and status.

Evidence is not the crux

A project may establish many true statements near an open theorem.

For Li’s criterion, 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 evidence.

Proving $\lambda_2 > 0$ is more evidence.

Checking the first million coefficients numerically is substantial evidence.

None of those statements proves:

$$\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]

The software needs to preserve that gap.

A finite-check function should return a finite-check result. It should not inhabit the type representing universal positivity. A theorem about a prefix should not be coerced into a theorem about the sequence.

This sounds obvious in prose. Type boundaries are how it stays obvious after years of refactoring.

Encode “open” as data

A research repository often uses status words:

• established
• partial
• conjectural
• open
• refuted

Those words should not live only in a README.

The central proof can be represented as an absent value:

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

or the equivalent in the proof assistant’s model.

If the crux is open, proof is None.

Not a fake inhabitant.

Not a theorem behind an unchecked axiom.

Not a boolean named is_proven set from the number of passing examples.

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 the status claims exists.

A generated report can then say:

• the analytic constant is constructed
• this finite coefficient is positive
• the bridge interface is formalized
• the universal positivity proof is absent
• RH remains open

That is more informative than an all-or-nothing project badge.

Do not use sorry as a project-management tool

Proof assistants allow placeholders during development. Lean’s sorry is useful while sketching a theorem.

It is dangerous when the repository’s public status treats the file as proved because it elaborates.

There are several honest patterns:

1. keep the theorem statement in an explicitly conjectural namespace
2. represent the missing proof as data rather than a theorem
3. make CI reject sorry in established modules
4. separate 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 repository can still build useful code around the conjecture. It just cannot let the conjecture cross into the established layer unnoticed.

Formalize the mechanism before claiming the object

An open construction often has a known shape.

The function-field mechanism may identify the kinds of objects and theorems a number-field analogue would need. Formalizing that mechanism is useful even when the analogue is missing.

It can establish:

• the input assumptions
• the type of intersection pairing required
• the positivity statement
• the implication from those assumptions to the spectral conclusion
• which exact assumption remains unavailable

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]

A conditional theorem is not a solution. It is still valuable.

It prevents the project from repeatedly arguing informally about what would be sufficient. It turns “we need some geometry here” into a list of proof obligations.

Build infrastructure without pretending it closes the theorem

Ambitious theorem work requires a lot of machinery:

• exact rational arithmetic
• constructive real and complex numbers
• convergence
• transcendental functions
• zeta functions in specified regions
• arithmetic functions
• finite identities
• formal algebra
• tactics and normalizers

Each component can be genuinely useful and genuinely proved.

The repository should state its range precisely.

For example:

• constructing $\zeta(s)$ in the half-plane where a series converges is not analytic continuation to the critical strip
• constructing an approximation to $\Gamma$ is not a proof of every identity needed later
• proving finite instances of Li positivity is not Li positivity for all $n$
• defining a candidate square is not proving the required universal property
• proving the universal 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]

The supporting mathematics is not diminished by saying where it stops.

It becomes reusable.

Status names need local meaning

Words such as “complete” are dangerous in multi-stage research.

“Stage B complete” may mean every task defined for Stage B has landed. A casual reader may hear “the mathematical program is complete.”

A better status line names the scope:

Stage B implementation checklist complete; central theorem remains open.

The status model can include both dimensions:

implementation: complete
verification: partial
research claim: open

This is the same separation I want in systems repositories:

• code exists
• tests pass
• external conformance passes
• performance target is measured
• product hypothesis is supported

One green word cannot carry all of those meanings.

Counterexamples should remain first-class

A formal research program becomes stronger when it records the constructions that do not satisfy the target property.

A counterexample can show that:

• a proposed positivity statement is too weak
• a spectrum mapping loses necessary information
• a candidate product collapses dimension
• a finite criterion does not control the universal case
• a computational 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.

In a long-running project, the counterexample is often the most reusable result.

External readers need an honesty map

A repository working near a famous open problem attracts attention from people with very different backgrounds.

The project should make it easy to answer:

• What is proved by the kernel?
• What depends on an assumption?
• What is numerical evidence?
• What is a candidate construction?
• What is refuted?
• What remains the central open obligation?

A proof-status matrix is not an apology. It is navigation.

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]

The more ambitious the project, the more important that map becomes.

The repository should make overclaiming difficult

The strongest version of research honesty is mechanical.

CI can enforce that:

• established theorem modules contain no placeholders
• open claims cannot be exported as proved values
• generated documentation reads the status ledger
• finite checks cannot inhabit universal proof types
• dependency graphs show which results rely on assumptions
• claims marked refuted cannot remain enabled as defaults
• every public status has a source artifact

This does not prove the theorem.

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

That is an important property.

Open problems still support real engineering

There is a false choice between solving the famous theorem and doing nothing useful.

A careful research program can produce:

• verified mathematical libraries
• clearer formulations of the missing construction
• reusable conditional mechanisms
• counterexamples
• computational evidence
• better proof tooling
• a durable map of open obligations

The project remains worthwhile even if the central theorem stays open.

The key is to let each artifact claim exactly what it establishes.

Build the machinery.

Name the missing object.

Record the evidence.

Keep the crux open until there is a proof term that closes it.