Formal Verification and Machine-Checked Proof

Key Takeaways

‍

• A machine-checked proof is one whose every step has been validated by a program rather than accepted by a reader.
• The guarantee it provides is different in kind from peer review: the checker confirms that each inference follows from stated rules, and it has no notion of a step being obvious enough to skip.
• Most published mathematics is written for humans and leaves routine steps implicit. Formalising it makes every omission explicit, which is why the process is slow and why it occasionally uncovers gaps that review did not.
• Aristotle is built for long-horizon formal reasoning and proof-oriented work. Its outputs stay provisional until independently checked or formally verified, and the research ledger keeps known, provisional, rejected and verified results distinct.

‍

What Formal Verification Means

In one sentence - the practice of writing a mathematical argument in a language precise enough that a computer program can confirm every step of it. The idea is old, was met with early scepticism, and is now routine in the places where correctness matters enough that arguments are checked rather than reviewed before anything is built on them.

Large formalisation efforts have shown that results of real depth can be carried all the way through a proof assistant without a single step left implicit, which shifts the question from whether formal proof is feasible to where it is worth the cost.

A proof assistant is a program holding three things: a formal language, a fixed set of inference rules, and a checker. A human — or an agent — writes the argument in that language; the checker confirms that every line follows from earlier lines and from the axioms, and rejects anything that does not. The output is not a judgement about whether the argument is convincing or elegant or important. It is a mechanical confirmation that the chain of inferences is complete, with no missing links. What the checker cannot do is tell you that the statement you formalised is the statement you meant, which is where the remaining human responsibility sits.

Nomos is organised around this standard: research records are published as they are produced, and nothing is promoted to settled without verification. The problem the process is currently applied to is the Strong Goldbach Conjecture.

‍

Why a checker beats a careful reader

Peer review is not a weak process, and the overwhelming majority of the mathematics it has certified is correct. But it is a human process with human failure modes, and the guarantee it offers is different from the one a checker offers. Four differences account for most of the gap between them.

‍

Nothing is obvious

A referee reads with context. Steps that are standard in the field are accepted without expansion, and that is what makes reading a paper possible at all. A checker has no context: every step must be spelled out, including the ones everyone in the field would skip. This is the main reason formalisation is slow, and also the main reason it finds things. Gaps in published arguments are rarely dramatic errors; they are usually a step that looked routine and was not, or a case assumed to be symmetric to another when it was not. Such gaps survive review precisely because they look unremarkable, and they do not survive mechanical expansion. The cost is real: formalising a substantial result can take far longer than writing it did, which is why the practice has spread unevenly across mathematics rather than all at once.

‍

The guarantee is checkable

A formal proof does not have to be trusted on anyone’s authority. The proof object can be re-checked by an independent implementation, by anyone, at any time, without their having to understand the argument. That is a far weaker demand on the reader than review makes, and a far stronger guarantee in return. The trust that remains sits in the checker itself and in the statement of the theorem, both of which are small enough to inspect directly.

‍

It scales past human patience

Some arguments are long, repetitive, and full of cases that differ only in detail. Human review of such material is unreliable in a predictable way: attention degrades exactly where the cases become mechanical and interchangeable. A checker does not lose attention, and it treats the ten-thousandth case with the same rigour as the first. This is one of the few places where machine checking has an absolute advantage rather than a marginal one.

‍

It composes

Informal results compose badly. Building on a paper means inheriting whatever it left implicit, and an omission that is harmless in isolation can turn out to be load-bearing several results later. Formalised results compose cleanly: once a theorem is in the library, anything built on top of it inherits a verified dependency rather than an assumption. Over a long research programme this is the difference between a growing base and a growing liability.

‍

What Machine Checking Does Not Give You

It is worth being equally precise about the limits, because formal verification is often described as though it removed all doubt. It does not. It removes one specific class of doubt — whether the steps follow — and leaves three others exactly where they were before.

‍

Three residual risks

Statement risk: A checker verifies that your proof establishes your formal statement. It cannot tell you that your formal statement means what you intended in ordinary mathematical language. A subtly mis-stated hypothesis produces a perfectly valid proof of the wrong theorem, and this is the failure mode formalisation is least able to catch. In practice it is managed by stating theorems in as standard a form as possible, and by having the statement, if not the proof, read by people.

Checker risk: The checker is itself a program and could contain a bug. The usual mitigation is architectural: the trusted part is kept small — a kernel that everything else must route through — so that it can be audited directly and re-implemented independently. The residual risk is not zero, but it is concentrated in one small, heavily examined component instead of being spread invisibly across an entire argument.

Scope risk: A verified theorem is verified under its own hypotheses and nothing more. It is easy to read a formal result as settling more than it does, particularly when the hypotheses include a qualifier such as sufficiently large, or exclude a class of cases that looked unimportant at the time. Formalisation makes those conditions explicit rather than removing them, which is an improvement — but only if the conditions are actually read. Most of the misreporting around open problems comes from this, not from anyone doubting the underlying proof.

None of these is an argument against machine checking. They are the reason a verified result is still recorded as verified rather than as final, and the reason the statement being verified is published alongside the verification instead of summarised.

The alternative is worse in every respect. An informal proof carries all three of these risks plus the one that formalisation eliminates, and it distributes them invisibly across every step a reader chose to accept. The choice is not between certainty and doubt; it is between doubt that is located and doubt that is not.

What a long research programme needs is a way to accumulate results without accumulating unverified assumptions alongside them, and to know at any moment which is which.

That is what formalisation provides.

‍

‍

‍

‍

How This Connects to Aristotle

Aristotle is an autonomous research agent built by Harmonic, a company co-founded by Vlad Tenev and Tudor Achim with the stated aim of building mathematical superintelligence. The agent is designed for long-horizon formal reasoning and proof-oriented work, and it is the reasoning engine recorded in the Nomos research ledger, which logs what the process is doing while it runs rather than after a conclusion has been reached.

Three properties of that design matter for verification work specifically, and each is a consequence of building for proofs rather than for fluent prose.

‍

Proof-oriented output

The target is not a persuasive explanation but an artefact a checker will accept. That changes what counts as progress: a step that reads well but cannot be formalised is not progress, and a step that formalises but reads awkwardly is. Work of this kind is produced against a formal language and its inference rules rather than against a reader’s judgement, and the difference shows up mostly in what gets discarded.

‍

Long-horizon reasoning

Open problems are not solved in one pass. They require holding a large amount of context, trying an approach, recognising that it fails, recording why it failed, and then continuing from that state rather than from the beginning. Most language models are optimised for short interactions and lose coherence over exactly the horizons this work needs. An agent designed for long-horizon reasoning is designed for the opposite: continuity across long stretches, explicit state, and failed branches kept on the record, because knowing what does not work is part of the map.

‍

Provisional until checked (the default status)

Every new claim the process produces enters the ledger as provisional. It stays there until it has been independently checked or formally verified, regardless of how strong the supporting evidence looks. This is deliberately conservative, and it is the reason the ledger is described as a set of research records rather than a series of announcements. Known results, provisional claims, rejected lines of argument and verified outputs are kept in separate categories, and nothing is promoted between them quietly. A claim that never leaves the provisional column is still a useful record.

‍

What Gets Recorded

‍

• Known results [reconstructed]: ​​Existing partial results on the problem, restated so that every hypothesis is explicit, including the conditions under which each one stops applying. A reconstruction is not a new theorem and is never recorded as one.
• Provisional claims [unchecked]: Statements the process currently supports but which have not yet been independently checked or formally verified. These are published as they arise, with their status attached.
• Rejected lines [kept]: Approaches that were tried and failed, retained rather than deleted, because a recorded dead end is information the next attempt does not have to rediscover.

‍

‍

‍

Verification Compared

There are three ways a mathematical claim can be certified, and they are not interchangeable. Numerical evidence checks the statement on a finite range. Peer review checks the argument against a specialist’s judgement. Machine checking checks the argument against a fixed set of rules. Each answers a different question, and each has a failure mode the others do not share. The following summarises where they differ.

‍

‍

The comparison is not a ranking. Numerical evidence remains the fastest way to find a counterexample, and review remains the only one of the three that asks whether a result is worth having at all. Machine checking is the only one that can certify an argument outright, and it certifies nothing else.

In practice all three are used together. Verification at scale suggests where a statement is likely to hold, and occasionally kills it outright. Heuristic and analytic work suggests why it should hold. Formalisation settles whether a specific argument for it is sound. Aristotle’s work sits mainly in the third layer, with the first two treated as inputs rather than conclusions. Reconstructing the known boundary of the Strong Goldbach Conjecture means moving the existing literature into that third layer, so that anything built afterwards rests on checked ground instead of on a summary of it.

‍

Conclusion

The question of what counts as a proof has a precise answer, and it has not changed: a complete chain of inferences from stated axioms. What has changed is who is able to check the chain. Machine checking removes the reader from that role and replaces them with a program that has no sense of which steps are important, which is exactly the property that makes it useful. It does not make mathematics certain. It makes the remaining uncertainty locatable.

For an open problem this matters more than it does for settled mathematics. A claimed resolution of a long-standing conjecture attracts attention far faster than it can be evaluated, and the gap between announcement and assessment is where most of the damage gets done. A process that publishes its intermediate state, marks every output with its status, and treats verification as a precondition rather than a formality is slower and much less quotable. It is also the only kind of process whose record can be read years later without having to reconstruct what was actually known at the time. Nothing here is claimed as proven. That is the point.

‍

Resources

• Harmonic: Official Website
• Proof assistants: Background on interactive theorem provers
• Formalisation projects: Notes on the cost and pace of large formalisation efforts
• Nomos: Official Website
• The Strong Goldbach Conjecture: Statement and standard formulation
• Numerical verification: How exhaustive checking is carried out at scale
• Partial results: Where the known boundary currently sits
• The ternary case: Why the odd, three-prime version behaves differently from the even one
• The circle method: The analytic approach used for additive prime problems
• Trusted kernels: Why proof checkers keep their trusted base as small as possible
• Aristotle: Overview of the research agent
• Research ledger: Official Website
• Formal languages: Getting started with machine-checked proof
• Statement risk: Why formalising the wrong statement is the hardest failure to catch
• Provisional & verified: Why new claims are not treated as settled before independent checking or formal verification
• Nomos on X: Where research updates are recorded