Reading OpenAI’s Math Repository: From Research Claims to Checkable Proofs

A mathematical claim does not become a theorem because it sounds convincing, survives a thousand examples, or appears in a repository with an impressive name. It becomes a theorem when a valid proof establishes precisely what the claim says, under precisely the assumptions it needs.

That distinction is the best starting point for exploring OpenAI’s math repository. This is a collection of mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model. Some entries have associated Lean formalizations; others do not. The repository is unusually interesting because it lets readers move between human-readable arguments, formal statements, and infrastructure for checking selected proofs.

But those layers must not be collapsed into a single verdict. A manuscript is not automatically a verified result. A formal proof establishes a formal statement, not whatever a headline might suggest. A successful check also depends on definitions, assumptions, and the checking environment.

This guide explains how to read the collection without either dismissing it or mistaking its catalogue for a list of independently established breakthroughs. We will build the necessary vocabulary, work through two mathematical intuitions, and follow the evidence from a paper to its formal verification boundary.

Source snapshot: Repository-specific descriptions below were checked on 7 October 2026, at commit adc7f1241b42e322a6451854ab7e4b4c146bf78a. Counts and research claims are attributed to that snapshot. This article is an explanatory source review, not an independent validation of the claimed research results; no Lean build or Comparator verification was run for it.

Topic index and reading paths

1. Proofs, conjectures, and tests
2. What the repository releases
3. A practical map of the collection
4. The disclosed process versus a learning workflow
5. Worked intuition: approximating pi
6. Worked intuition: zeta and zero-free regions
7. How Lean turns propositions into checkable objects
8. Comparator and the remaining trust boundary
9. A bounded reproduction path
10. Limitations and implications
11. Glossary
12. Exercises with answer sketches
13. Primary sources and further reading

Beginner path: Read sections 1–3, then the pi and zeta examples. Use the glossary whenever a term interrupts the argument. Finish with the trust-boundary discussion before drawing conclusions about the release.

Technical path: Start with the repository map, follow one family into its scope documentation and Comparator configuration, then read the Lean and reproduction sections. Keep the informal theorem beside the formal statement.

The mathematical examples are teaching illustrations, not reconstructions of the repository’s research proofs. Short sections, explicit symbols, and labelled figures are intended to make this a reference you can revisit rather than a wall of theorem names.

Proofs, conjectures, and tests

A proposition is a statement that can be true or false. “Every even integer is divisible by two” is a proposition. “Find an interesting pattern” is an instruction, not a proposition.

A conjecture is a proposed mathematical statement for which a proof has not been established. Evidence may support it, sometimes overwhelmingly. A theorem is a statement established by a proof within stated assumptions and a mathematical foundation. A proof supplies a logically justified route from those assumptions to the conclusion.

The difference from software testing is easiest to see in a toy example. Consider the claim that

is prime for every nonnegative integer $n$. Testing $n=0$ gives $41$; testing $n=1$ gives $43$. In fact, all inputs from $0$ through $39$ give primes. That is an impressive run of examples, but at $n=40$,

One counterexample defeats the universal claim. Forty successful tests did not establish it.

Now compare a genuine elementary proof: every odd integer has an odd square. Write an arbitrary odd integer as $n=2k+1$, where $k$ is an integer. Then

The final expression is odd by definition. Unlike testing a collection of inputs, the argument covers every allowed $k$ at once.

Tests remain valuable. They can expose mistakes, suggest conjectures, and check finite subproblems. A rigorously justified exhaustive computation over a finite domain can even form part of a proof. The key question is whether the computation covers everything the statement quantifies over, with a trustworthy connection between the implementation and that statement.

Why research mathematics is not another benchmark

Many mathematical benchmarks use curated problems with known answers and relatively stable grading procedures. Research problems can lack an agreed solution, depend on substantial literature, or conceal ambiguity in their formulation. Progress might mean a counterexample, a weaker theorem, an additional hypothesis, or a new tool—not simply a correct final number.

The repository’s README says OpenAI expanded evaluation on open research problems after performance on existing mathematical evaluations saturated. That explains the stated motivation, not an automatic measure of research competence.

Research evaluation must ask more than “Did the answer match?” It must ask: Is the statement new? Are the hypotheses sufficient? Does the proof use an unproved intermediate claim? Is a cited theorem applicable? Does the result say what the surrounding prose implies?

Those questions explain why this release is better approached as an inspectable research collection than as a scoreboard.

What the repository releases

The README describes 722 manuscripts organized into 372 result families at the snapshot reviewed here. A family groups related papers: a principal result, companion arguments, consequences, or alternative proofs. A manuscript is an individual document. Neither is necessarily equivalent to one posed problem or one independent discovery.

The distinction matters even before any mathematics is checked. Two manuscripts might develop the same central argument in different directions. A later paper might build on an earlier model-produced result. Counting documents therefore answers a different question from counting independent contributions.

The released materials include:

• An overview and manuscript map, providing family descriptions, paper titles, abstracts, and links.
• Preprints, including PDFs, source files, and manuscript-specific citation and build instructions.
• A Lean library, containing formalizations of some results.
• Formalization metadata and scope notes, connecting selected mathematical claims to declarations and checking configurations.
• Comparator challenges, defining formal targets and how selected solutions are to be checked.
• Abridged reasoning summaries for ten selected families, including the pi example discussed below.

“Abridged” is important. These summaries should not be described as complete execution logs or a reproducible record of every prompt, tool call, rejected attempt, and intermediate state.

This is not a model SDK, a model-weights release, or a training repository. Its published proof artifacts are not an interface for invoking the internal model. Availability of a manuscript or Lean file does not mean readers can rerun the original model-generation experiment.

What the production numbers do—and do not—say

According to the README checked on 7 October 2026, the vast majority of results used the same procedure with an unreleased internal OpenAI model. It reports an average of three hours of ChatGPT Pro thinking compute per result, and says the model was posed approximately 4,000 problems over the evaluation.

The README also says aggregation into families and manuscripts, together with a significance requirement, produced the published catalogue. It identifies exceptions to the fixed procedure, including zeta zero-free-region work and work concerning the Hodge conjecture for CM abelian varieties. The writeup for the zeta region $\operatorname{Re}(s)>11/12$ was human edited for readability.

These are publisher-reported process descriptions, not measurements independently reproduced here. The units “problem,” “result,” “family,” and “manuscript” do not define a common denominator. The release therefore does not support deriving a success rate from these headline counts, or a total-compute estimate from the reported average.

Most importantly, the README explicitly describes different stages of verification, warns that some unformalized results could have issues, and promises versioned corrections. Those qualifications belong beside the counts, not in a footnote after them.

A practical map of the collection

Opening hundreds of PDFs is not a reading strategy. Choose one mathematical question and follow its evidence trail.

A useful first destination is family 017, concerning the irrationality exponent of pi. Its scope page explains the selected formal statement and explicitly says that the paper’s Flint–Hills series consequence is outside that selected statement. That is much more informative than a bare “Lean available” label.

For a concrete machine-readable route, examine the zeta entry in the formalization catalogue. It identifies:

• Declaration: OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re
• Source file: OAI/NumberTheory/DirichletL/Nonvanishing.lean
• Configuration: ComparatorChallenges/QuasiRiemannHypothesis.json

The catalogue says paths are relative to lean/, and its overall scope is labelled “Partial progress.” Its review metadata also says status: unchecked. That is a metadata status, not a compiler failure or evidence of a mathematical error. Treat each mapping as a pointer to inspect, not as a substitute for running the relevant checks.

Keep a small reading record: commit, family number, manuscript version, informal theorem, formal declaration, assumptions, verification performed, and unresolved questions. This prevents a surprisingly common error: attributing one version’s statement or one selected theorem’s verification status to an entire family.

When returning later, follow the family number and saved commit rather than relying on a title remembered approximately. The repository promises to preserve public release history and record corrections as new versions. That makes version-specific reading and citation part of responsible interpretation.

The disclosed process versus a learning workflow

It is tempting to turn a collection like this into a cinematic pipeline: the model receives a conjecture, invents a proof, translates it into Lean, fixes every error, and publishes a theorem. The README does not disclose that complete sequence as the uniform production method.

What is disclosed: an internal unreleased model; a largely shared procedure; the reported average thinking compute; approximately 4,000 posed problems; selection and aggregation into the catalogue; some results building on earlier model outputs; selected abridged reasoning summaries; exceptions and one identified human-editing intervention; and uneven formalization coverage.

What follows is a generic explanatory workflow, useful for understanding mathematical verification. It is not a claim about the undisclosed details of OpenAI’s process:

1. Specify the problem. State the objects, assumptions, and desired conclusion.
2. Develop a candidate argument. Search for constructions, lemmas, reductions, or counterexamples.
3. Challenge the argument. Test special cases and inspect every cited or newly asserted dependency.
4. Write a complete manuscript. Make quantifiers, exceptional cases, and dependencies explicit.
5. Formalize a selected statement. Translate definitions and claims into a proof assistant.
6. Construct and check the proof. Produce proof terms, inspect assumptions, and verify against the intended formal target.
7. Review alignment and significance. Ask whether the formal target matches the mathematical claim, and what the result adds.

Figure 1. Published artifacts and a generic verification workflow are different kinds of information. The explanatory steps are not a reconstruction of the repository’s undisclosed generation procedure.

Real mathematical work loops between these steps. A failed formalization may reveal a missing assumption in a paper. An attempted proof may produce a counterexample instead. An expert may discover that a valid formal theorem captures only a narrower statement.

To see why these distinctions matter, let us unpack two catalogue topics without pretending to reproduce their research arguments.

Worked intuition: approximating pi

Pi is irrational: it cannot equal a ratio of integers. Yet some rational numbers approximate it remarkably well. The research question in family 017 concerns the long-term limits of that approximation, not merely finding another useful fraction.

Let $p$ be an integer and $q$ a positive integer. Define the absolute approximation error

The denominator $q$ measures one kind of complexity: roughly, how fine a rational grid we allow. An error of one millionth is impressive with a small denominator but less surprising with an enormous one.

Here are familiar examples. The displayed values are rounded evaluations of the actual absolute error, not estimates obtained from $1/q^2$.

The last fraction is unusually good for its denominator. In the plot below, compare its point with the reference curve at the same horizontal position: the vertical separation shows how much smaller its error is than the comparison scale. Both axes are logarithmic, so equal visual distances represent equal ratios, not equal absolute differences. But “unusually good” is not the same as “representative of all large denominators.”

Figure 2. A teaching comparison, not a model benchmark. Points represent $|\pi-p/q|$ for the four labelled fractions; the reference curve is $1/q^2$. Both axes are logarithmic. The errors are defined by the exact expression, with numerical rendering and table values rounded.

From a good fraction to an exponent

For an irrational real number $x$, its irrationality exponent measures how strong an approximation inequality can hold infinitely often. One standard formulation is

Here $\nu$ is a real exponent, “reduced” means numerator and denominator have no common factor, and $\sup$ means least upper bound. Requiring infinitely many distinct fractions prevents one spectacular approximation from deciding the answer.

For $q>1$, increasing $\nu$ makes $q^{-\nu}$ smaller, so the required approximation becomes more demanding. Classical rational-approximation theory guarantees every irrational number infinitely many approximations at the $1/q^2$ scale. Thus an exponent of two is a natural threshold, not an arbitrary constant chosen for this repository.

The family 017 scope note reports the claim $\mu(\pi)=2$. In particular, it describes the eventual lower bound

with positive integer denominators. This is a repository-reported research claim, not a result independently validated by this article.

Read the quantifiers slowly. Choose any positive tolerance $\varepsilon$. There must then be a threshold $Q$, possibly depending on that tolerance. Beyond it, no numerator $p$ gives an approximation beating the stated power. The claim does not say the bound holds for every small denominator, that one threshold works for every $\varepsilon$, or that the scope note supplies a practical numerical threshold.

Our four fractions cannot establish this assertion. Even a graph with millions of points would not control every sufficiently large denominator. Conversely, the exceptional accuracy of $355/113$ does not refute an eventual statement: a finite collection of exceptions can lie below $Q$.

Why a series appears nearby

The manuscript map also associates the claim with convergence of the Flint–Hills series,

where angles are in radians. The intuition is that $\sin n$ becomes small when an integer $n$ lies very close to a multiple of pi. Such near-coincidences are related to rational approximations to pi. Small denominators inside the summand can create large spikes, so controlling approximation quality helps control them.

That is a motivation, not a proof of convergence. The scope page explicitly excludes this consequence from its selected statement. It demonstrates why the unit of verification must be the named theorem, not every sentence surrounding it.

Worked intuition: zeta and zero-free regions

The second example moves from rational numbers to the complex plane. Write

where $\sigma$ and $t$ are real numbers and $i^2=-1$. The real part is $\operatorname{Re}(s)=\sigma$; the imaginary part is $t$.

For $\sigma>1$, the Riemann zeta function is defined by the absolutely convergent series

For example, $\zeta(2)=1+1/4+1/9+\cdots$. But the region relevant to famous questions about its zeros lies partly outside that series’ domain of convergence.

The analytic-continuation caveat is essential: outside $\operatorname{Re}(s)>1$, the displayed infinite series is not a general recipe for evaluating zeta. The function is extended by analytic continuation. This extension is meromorphic: it is analytic except for a simple pole at $s=1$. A pole is a singularity, not a zero. The NIST Digital Library of Mathematical Functions supplies the standard definitions.

Why primes enter the picture

In the region $\sigma>1$, zeta also has the Euler product

Here the letter $p$ ranges over primes, rather than serving as the arbitrary numerator it did in the previous section. Expanding each factor as a geometric series and using unique prime factorization explains the bridge between a sum over all positive integers and a product over primes.

Absolute convergence is doing real work. Merely observing that each factor is nonzero would not prove that an arbitrary infinite product is nonzero. In this region, the convergence theory justifies the product and its nonvanishing.

Consequently, the half-plane $\sigma>1$ is classically zero-free. Standard theory also excludes zeros on the line $\sigma=1$, with the pole at $s=1$ handled separately. The nontrivial zeros lie in the critical strip

The Riemann hypothesis asserts that every nontrivial zero lies on the critical line $\sigma=1/2$. Negative even integers give the familiar trivial zeros outside this strip. These are standard background facts, distinct from the repository’s new claims; see DLMF’s account of zeta zeros.

What a fixed zero-free region would mean

A claim that zeta has no zeros in $\sigma>\theta$, for a fixed $\theta<1$, excludes a vertical portion of the critical strip at every height $t$. It is not merely a statement about zeros below some computational cutoff.

For instance, $11/12\approx0.9167$. A boundary there would exclude zeros to its right while leaving a substantial part of the strip unexcluded by that assertion. It would not establish that every nontrivial zero lies on $1/2$. Read the figure horizontally to compare those boundaries, then remember that the assertion extends vertically to every height—not just the portion a finite drawing can show. The empty region is an illustration of the claim’s scope, not evidence obtained by searching it.

Figure 3. Geometry, not measured zeros. The $11/12$ boundary is shown only as a repository-reported claim, not an independently validated result. The classical region $\operatorname{Re}(s)>1$ is distinguished from that claim; the singular point $s=1$ is a pole, not a zero. No zero measurements are plotted.

There is a version-sensitive detail worth noticing. The README specifically mentions a human-edited $11/12$ writeup. Meanwhile, family 003 in the manuscript map lists a $7/8$ claim and an alternate $11/12$ proof; its Lean scope note describes selected $7/8$ statements. The reviewed Comparator configuration targets the $7/8$ zeta declaration.

Because $7/8<11/12$, a zero-free half-plane to the right of $7/8$ would be larger, and hence a stronger exclusion. These are distinct statements and artifacts. A figure explaining the README’s $11/12$ reference must not silently present that boundary as the exact target of the reviewed $7/8$ configuration.

We are describing what the collection reports, not adjudicating either proof. This example teaches two habits: keep a function’s domain and continuation straight, and compare the exact inequality in the manuscript with the exact inequality in the formal target.

How Lean turns propositions into checkable objects

Lean is both a programming language and an interactive theorem prover. Its relevance here is not that it can generate plausible mathematical prose. It gives mathematical statements and proofs a representation that a checker can inspect.

At a first approximation, propositions are types, and proofs are terms of those types. If $P$ is a proposition, a term with type $P$ is evidence establishing $P$. Lean places propositions in Prop.

Consider the elementary implication “if $P$ and $Q$, then $P$.” A schematic Lean example is:

example (P Q : Prop) (h : P ∧ Q) : P := h.left

P and Q are propositions. The input h is a proof of their conjunction. Its .left component is a proof of P. The expression is not testing whether two Boolean values happen to be true; it expresses a proof valid for arbitrary propositions and a supplied proof of their conjunction. This is an explanatory snippet, not a build result from this article.

Proof terms, tactics, and the kernel

Writing every proof term directly would be tedious. Tactics are programs that help construct those terms: applying existing lemmas, simplifying expressions, splitting cases, and solving routine goals.

A useful separation is:

• The tactic searches for or constructs a proof.
• The resulting proof term is the object to be checked.
• The kernel checks that the term has the claimed type according to the logical rules and declared environment.

An ordinary tactic does not become an authority merely because it says “done.” Its output must pass checking. This separation is why powerful automation can assist theorem proving without making every heuristic part of the core logical checker.

The word “kernel” should not suggest magic or absolute infallibility. It is software implementing a formal system. The relevant assurance is that a particular proof term checks against a particular statement and environment, with specified assumptions.

Axioms and unfinished proofs

An axiom is accepted as a foundational assumption rather than proved within the development. The reviewed zeta and pi Comparator configurations permit propext, Quot.sound, and Classical.choice: propositional extensionality, quotient soundness, and classical choice. These are standard Lean foundations discussed in Lean’s documentation, not permissions to assume the desired research theorem.

A different issue is sorry, Lean’s placeholder for a missing proof. It lets a development remain usable while unfinished, but creates a dependency on sorryAx. Successful ordinary compilation alone must therefore not be advertised as proof completeness.

There is an important wrinkle in this repository: the challenge files intentionally contain sorry. Their role is to specify the theorem that a separate solution must prove. Finding a placeholder in a challenge is not, by itself, evidence that the solution is unfinished. The question is whether the selected solution and its transitive dependencies use only the permitted axioms.

Likewise, a theorem can be perfectly valid but conditional on a very strong hypothesis. A statement of the form “if the conjecture holds, then the conjecture holds” is easy to prove and mathematically unhelpful. Verification must inspect the proposition, not merely the existence of an accepted proof term.

Comparator and the remaining trust boundary

Two Lean files can contain theorem names that look identical while referring to different underlying definitions. Checking only a name, a printed statement, or a build exit code does not fully address that risk.

The Comparator project describes a stronger comparison. Under its documented assumptions, it compares challenge and solution environments, checks the relevant statement dependencies, restricts axioms to an allowlist, and replays the solution environment through the Lean kernel. Its role is to establish that the supplied solution proves the specified formal target, rather than a conveniently altered one.

For the reviewed zeta configuration, the target is OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re. The JSON names separate challenge and solution modules, lists the three permitted axioms above, and sets enable_nanoda to false. This configuration does not request the optional Nanoda checker. No multi-kernel validation should be inferred from it.

In the figure below, follow the formal statement toward proof-term checking, then return to the separate statement-alignment branch. Comparator strengthens the first route; it cannot make the second unnecessary. The pi quantifier order and the two zeta boundaries show why: a proof can check successfully while a reader has attached it to a different claim.

Figure 4. Kernel checking and statement-alignment review answer different questions. Comparator strengthens the formal checking path; expert review still has to assess the translation from mathematical intent to the formal target.

Three questions, not one green tick

Is the derivation valid? Kernel checking addresses whether the proof establishes the formal proposition under the accepted foundations.

Is it the intended proposition? Statement-alignment review examines definitions, quantifiers, domains, coercions, side conditions, and exceptional points. The pi example’s “for every exponent, there exists a threshold” must not become “there exists one exponent.” For zeta, analytic continuation and the convention used to represent the pole require attention. Formal libraries commonly represent functions as total functions, so treatment of a mathematically singular input needs explicit interpretation.

Is the result significant and correctly situated? Novelty, relationship to prior work, and whether a manuscript’s consequences follow are mathematical-review questions. Neither type checking nor statement comparison settles them automatically.

Comparator also has operational assumptions. Its documentation discusses trusted challenge imports and project configuration, sandboxing through Landrun, compatible export tools, and a correct kernel. The operating system, hardware, caches, and an uncompromised checking environment remain relevant. Its current README includes additional sandbox-hardening guidance beyond the math repository’s short invocation.

The practical lesson is not that formal verification is futile. It is that formal verification provides a powerful, sharply defined assurance. Knowing its boundary lets us use that assurance rather than exaggerate it.

A bounded reproduction path

There are at least three distinct things a reader might try to reproduce: the model’s discovery process, the manuscript document build, or checking a selected formal proof. The released materials do not provide equivalent access to all three.

For formal checking, the Lean README recommends compiling small portions of the single large library. The repository’s Comparator README says to install comparator, landrun, and lean4export, make them available on PATH, and then run the following from lean/:

lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

These are the repository’s documented commands, reproduced here for reference—not a claim that they were executed successfully. They are also not a complete installation tutorial: the linked Comparator project supplies prerequisites, compatibility requirements, and security assumptions that should be read first. Use an isolated, nonprivileged checking environment and the applicable current upstream security guidance rather than treating downloaded proof projects as inert text.

Before running anything, inspect the selected configuration and corresponding challenge statement. After a run, preserve the source commit, tool versions, dependency state, complete command, output, and exit status. Since lake update can affect dependency resolution, record the resulting state rather than assuming the repository commit alone describes the full checking environment.

Two concrete details make that advice more than boilerplate. The math snapshot pins Lean v4.34.1, while the separately inspected Comparator snapshot pins v4.35.0-rc4; compatibility was not tested here, so installing the latest version of everything is not a verified recipe. Moreover, the math repository's Lake configuration contains executable dependency setup and applies repository-owned compatibility patches. Preserve those patches as well as upstream dependency commits. Their contents were not audited here, and none of those setup hooks was executed.

The Lean README warns that building the entire library may fail when Linux’s vm.max_map_count is too low. It mentions building Lean with -DMMAP=OFF, and potentially using GLIBC_TUNABLES set to glibc.malloc.mmap_max=0:glibc.malloc.arena_max=1. These are documented workarounds, not prerequisites to apply indiscriminately; the first recommendation remains to work on a small portion.

If a check succeeds, report exactly which configured theorem was checked and under what assumptions. If it fails, preserve the error and separate installation, resource, dependency, comparison, and proof-checking failures. Neither outcome alone gives a verdict on all 722 manuscripts.

Limitations and implications

The collection’s most useful feature is not its headline size. It is the possibility of linking a research claim to inspectable artifacts. That link supports criticism as well as confirmation.

Several limitations remain essential to any responsible interpretation.

Verification coverage is uneven. Some manuscripts lack formalizations. A selected formal theorem may omit consequences in the paper. A scope page or catalogue entry is documentation of intended coverage, not this article’s independent verification certificate.

The generation process is not fully reproducible from the release. An unreleased model and abridged reasoning summaries do not provide the complete experimental recipe. Proof-checking reproducibility and discovery reproducibility are different achievements.

Dependencies can connect apparently separate results. The README says some outputs build on earlier model results. Review should follow those dependencies instead of treating every manuscript as independent corroboration.

Research claims require specialist evaluation. A proof may be difficult to understand, a formal target may miss the intended meaning, or a claimed improvement may need qualification against existing literature. Public availability makes these questions examinable; it does not answer them.

Revisions matter. Corrections are compatible with serious mathematical work. What matters is whether changes remain traceable and whether readers can distinguish an earlier claim from its corrected form. The promised preservation of release history is valuable precisely for that reason.

For technical readers, a promising implication is a different division of labor. Models may help propose arguments and construct formal developments. Proof assistants can check specified derivations. Mathematicians can evaluate statement alignment, conceptual insight, and significance. None of those roles makes the others redundant.

There is also a lesson for evaluation design. If the target is research assistance, useful evidence includes a precise statement, a dependency trail, a checkable artifact, clear scope limits, and a correction history. A confident paragraph and a large count are weaker evidence than one carefully documented result.

The right stance is therefore neither “the repository proves everything it lists” nor “machine-produced mathematics cannot matter.” It is more demanding: choose a claim, understand it, inspect its artifacts, check what can be checked, and state the remaining uncertainty accurately.

Glossary

• Axiom: A foundational assumption accepted without an internal proof; its use should be explicit.
• Conjecture: A proposed mathematical statement not yet established by a proof.
• Theorem: A statement established by a valid proof under specified assumptions.
• Manuscript: An individual written paper; not necessarily an independent result.
• Result family: Related manuscripts grouped around a mathematical contribution or topic.
• Formalization: Encoding definitions, statements, and proofs in a formal system.
• Proposition: A statement that can be true or false; represented in Lean by a type in Prop.
• Proof term: A formal object whose type is the proposition it proves.
• Tactic: A program that helps construct proof terms.
• Kernel: The core component that checks formal derivations.
• Statement alignment: Whether a formal proposition faithfully captures the intended mathematical claim.
• Irrationality exponent: A measure of how accurately an irrational number admits infinitely many rational approximations.
• Analytic continuation: Extending an analytic function beyond an initial domain while preserving its analytic identity.
• Critical strip: The region $0<\operatorname{Re}(s)<1$ containing zeta’s nontrivial zeros.
• Zero-free region: A domain in which the specified function has no zeros, with singularities handled separately.
• Trust boundary: The line between what a checking procedure establishes and what it still assumes or leaves to other review.

Exercises with answer sketches

1. Repair an overconfident testing claim

A script checks the first million positive integers and finds no counterexample to a universal conjecture. What can it legitimately report?

Answer sketch: It can report no counterexample in the tested range, subject to implementation correctness. It cannot establish the universal claim unless a separate argument proves that this finite search covers every relevant possibility. Record the tested domain instead of replacing it with “all integers.”

2. Read the quantifier order

Explain the difference between “for every $\varepsilon>0$, there exists $Q$” and “there exists $Q$, for every $\varepsilon>0$” in the pi inequality.

Answer sketch: In the first, the threshold may depend on the requested exponent tolerance. In the second, one threshold must work simultaneously for every tolerance, a stronger demand. The selected scope statement has the first order. Moving quantifiers changes mathematics, even if all the same symbols remain.

3. Interpret the zeta picture

Suppose, hypothetically, a proof establishes no zeta zeros in $\operatorname{Re}(s)>11/12$. Does it establish the Riemann hypothesis? Can the original zeta series be used indiscriminately throughout that half-plane?

Answer sketch: No to both. The exclusion leaves part of the critical strip unrestricted by that assertion, while the Riemann hypothesis places every nontrivial zero on $1/2$. The defining Dirichlet series is valid for $\operatorname{Re}(s)>1$; the region between $11/12$ and $1$ requires analytic continuation or another valid representation. The pole at $s=1$ is handled separately.

4. Diagnose a placeholder without jumping to conclusions

You find sorry in a Comparator challenge. What should you inspect next?

Answer sketch: Determine whether the file is the trusted target specification or the proposed solution. Read the configuration, locate the solution module, and check permitted axioms and transitive proof dependencies through the documented checking procedure. A challenge placeholder is expected; an unpermitted sorryAx dependency in the selected solution is a different matter.

5. Design an honest verification report

What should a report say after successfully checking one configured theorem?

Answer sketch: Name the commit, declaration, challenge, solution, configuration, dependency and tool versions, commands, outcome, and permitted assumptions. State which alignment review was performed and what remains outside scope. Do not generalize one check to a whole manuscript family, the complete repository, or reproduction of the original model experiment.

Primary sources and further reading

Repository links below are pinned to the reviewed snapshot where applicable. Research claims in this article come from the publisher’s materials; the Lean and DLMF references explain established background rather than independently validating those claims.

1. OpenAI math README — release description, counts, reported procedure, qualifications, and version policy.
2. Manuscript map and overview — family structure, paper abstracts, and navigation.
3. Lean README and formalization catalogue — library guidance, declaration mappings, and checking configurations.
4. Repository Comparator README — the documented checking commands.
5. Pi scope note, challenge, and configuration — selected theorem and scope boundary.
6. Zeta scope note, challenge, and configuration — the selected $7/8$ target.
7. Comparator project documentation — comparison guarantees, prerequisites, and residual trust assumptions; consult its current version before use.
8. Lean: Axioms and Computation — foundations and the role of classical axioms.
9. NIST DLMF: zeta definitions and zeros — analytic continuation, the Euler product, and standard zero geometry.

For a particular manuscript, use the BibTeX supplied in its directory and identify the version you actually read. The most productive next step is small: choose one family and follow its statement all the way to the boundary of what its artifacts establish.