Certificates and checking
Every answer of Structure Computer carries a certificate. With it, anyone can confirm that the answer is correct without trusting the side that computed it. This document explains what certificates are for, what is in them, and how to check them again.
Why answers carry certificates
The part that computes the answers is large and complex, and may contain mistakes. Structure Computer is therefore built so that this part does not have to be trusted.
- Along with the answer, the computing part produces cheap hints to confirm it.
- The question, the answer, the hints, the presuppositions and the names of the theorems relied on go into a certificate.
- A separate program, the checker, re-checks the answer from the definitions, using only the certificate. The checker does not load the computing part's program.
- If the check fails, the answer is recomputed; if it fails again, the answer is “no result”, with the reason. An answer that has not passed the check is never returned as a certain answer.
Finding an answer is often hard even when confirming a correct one is easy. Certificates use that difference.
What is in a certificate
A certificate is a JSON document. Broadly, it contains:
| Content | Meaning |
|---|---|
| The question and its input | which question was asked, about which system, parameters, states and field |
| The answer (claim) | the answer itself, e.g. “t = σⁿ s ⇔ n ≡ r (mod M)” |
| The kind | certain, probably certain, reconstructed, statistical or no result, with the presupposition, assumption, error bound, statistic or reason where there is one |
| Hints | material for the checker to confirm the answer cheaply; the checker confirms each hint itself before using it |
| Theorem names | the names of the theorems, proved in Lean, that the answer rests on |
| Seed | the seed of the random choices made in the computation; the same seed gives the same certificate |
| Check record | how it was checked, such as how many times it was recomputed |
The checker also decides for itself which theorems must be cited, and requires the certificate's list to match exactly. It rejects a certificate whose outer statement of the answer differs from what its contents show.
What the trust rests on
| Answers | What is trusted |
|---|---|
| The main answers | theorems proved in Lean beforehand, saying “if the conditions the checker confirms hold, the answer is correct” (trusting Lean's kernel and the mathematical library Mathlib), and the checker |
| Id(s, t) for the Lyness map over 𝔽_q | in addition, it can be checked by a checking program whose own correctness is proved in Lean; then only Lean (including its compiler and runtime) and the part that reads the certificate are trusted |
| Probably certain | the check of a probabilistic proof given instead of following the orbit, and its bound on the chance of error |
| Statistical | not a theorem: the kind of the answer states that it is an estimate from samples |
To be candid: that the checker reproduces the definitions of the Lean theorems correctly is confirmed by tests, not proved. Some questions (part of the integrability verdict, for example) also have parts not proved in Lean, and that a probabilistic proof represents the orbit correctly is argued but is not a Lean theorem. Widening what the checker proved correct in Lean takes on is the way to make the base of trust smaller.
Checking again on the site
On the Try page a certificate can be checked again:
- From a result card: open the card's “Details”; “Check again with the checker” checks the same certificate again, and “Download certificate” saves it.
- By loading a certificate: open “Certificate check (tamper test)” at the bottom of the Try page, paste a certificate or load a file, and press “Check”. “Use the certificate last opened” puts in the certificate of the answer you last looked at.
- Tamper test: change one number in the pasted certificate (the step count of the answer, say) and check it: the checker rejects it, because the hints and the answer no longer agree.
- The Lean checker: “Also check with the Lean checker” checks Id(s, t) for the Lyness map over 𝔽_q with the checking program proved correct in Lean as well. Where that checker is not available on the compute server, it shows “unavailable”.
A saved certificate can be given to someone else, who can check it the same way.
What a certificate shows, and what it does not
- A certificate shows that “for this input, this answer holds”. A different input needs a different certificate.
- An answer with a presupposition holds under that condition.
- A reconstructed value is unique under the stated assumption (a bound on the size of the step count, say).
- A statistical answer is not a theorem.
- “No result” makes no claim; it gives only the reason.