The following problem (call it THEOREMS) belongs to class NP.


* **Input:** Mathematical statement $S$ (written in some formal system such as ZFC) and positive integer $n$ written in unary.
* **Output:** "Yes" if $S$ has a formal proof of length at most $n$. "No" otherwise.


It is known that there is an algorithm which, in a number of steps polynomial in $n$ (and in the length of $S$, which is usually negligible if $n$ is large), converts every instance of THEOREMS to an instance of (say) SAT.


My questions are the following: 


1. Has this algorithm been implemented in full generality? That is, I could download it, input my $S$ and $n$, press a button, wait for some time, and get an instance of SAT?
2. If not, is there at least theoretical analysis what could be the length of the resulting SAT in terms of $n$, $n^{100}$ or $n \log n$?
3. Erdos Discrepancy Problem, at least for discrepancy 2, has been [reduced to SAT](https://arxiv.org/abs/1402.2184). Are you aware about similar conversion of any other famous problem, like Riemann Hypothesis?


**Note:** I am not discussing how feasible would be to actually *solve* the SAT instance corresponding to "proving Riemann Hypothesis in a million of steps". My question is just about GENERATING this and similar SAT instances.



Representing mathematical statements as SAT instances
Improving on Brumleve's answer, I have a method for encoding a length-$n$ proof with a quasilinear $\tilde {O} (n)$-bit 3SAT instance.


In most formal systems, proofs and objects that appear in proofs (propositions, formulas, etc.) have a tree-like structure in that each such object can be built from other such objects in an enumerated list of ways. For example the proposition $P \to Q$ is built out of the two propositions $P$ and $Q$, and a proof of $Q$ can be made with modus ponens out of a proof of $P \to Q$ and a proof of $P$. Such a proof-tree can be encoded with a pointer architecture, as some sequence $x\_0, \dots, x\_{n-1}$ where each $x\_i$ encodes a formula or a proposition or a proof of a proposition, possibly encoding including references to earlier objects $x\_j$, $j < i$. For example, if $x\_k$ encodes the proposition $P \to Q$, which I will denote with the notation $k \mapsto (P \to Q)$, then $x\_k$ might have information of the form $(\to, i, j)$ where $i \mapsto P$ and $j \mapsto Q$. Similarly, denoting $k \vdash Q$ for $x\_k$ encoding a proof of $Q$, a proof $k \vdash Q$ by modus ponens might be given in the form $(\mathtt {ModusPonens}, i\_0, i\_1, i\_2, i\_3, i\_4)$ where $i\_0 \mapsto P$, $i\_1 \mapsto Q$, $i\_2 \mapsto (P \to Q)$, $i\_3 \vdash P \to Q$, and $i\_4 \vdash P$.


In addition, if $x\_j$ includes references $i\_0, \dots, i\_{k-1}$ to earlier objects, define $y\_j = (x\_{i\_0}, \dots, x\_{i\_{k-1}})$ as a description of all the objects referenced by $x\_i$.


To check if the objects $(x\_0, \dots, x\_{n-1})$ with the supplementary information $(y\_0, \dots, y\_{n-1})$ encodes a proof of the Riemann Hypothesis, you must check the following conditions:


* *(Local validity)* Each $x\_i$ represents a valid construction of a proof object out of earlier proof objects. For example if $x\_i = (\to, j, k)$ then it is necessary to check that $x\_j$ and $x\_k$ encode propositions and not some other kind of object. For steps such as modus ponens where it is necessary to check the syntactic equality of two subexpression, check for pointer equality of the corresponding objects instead. This change does not affect which statements we can prove in a given number of steps since it is always possible to deduplicate so that each syntactic expression appears at most once in the list $(x\_0, \dots, x\_{n-1})$, and this can only shorten the proof. If $x\_i$ is constructed with enough references then checking the local validity of $x\_i$ only requires $O (\log n)$ bit-operations on the inputs $(x\_i, y\_i)$, for a total of $O (n \log n)$ .
* *(Non-cyclicness)* If $x\_j$ contains references $i\_0, \dots, i\_{k-1}$ then we have $i\_0, \dots, i\_{k-1} < j$.
* *(Right conclusion)* $x\_{n-1}$ encodes a proof of the Riemann Hypothesis. One way to check this is to fix $x\_0, \dots, x\_{k-1}$ to hardwired constant values for some $k = O (1)$ so that $x\_{k-1}$ formulates a statement of the Riemann Hypothesis, and ask that $x\_{n-1}$ encodes a proof of $x\_{k-1}$.
* *(Correctness of $(y\_j)$)* The values $y\_k$ correctly dereference the references given in $x\_k$. The rest of my answer explains how to check this.


We've reduced the problem of checking proof validity to the following *reference-checking problem*: Given an array $x\_0, \dots, x\_{n-1}$ of $\ell$-bit values and a list $(k\_0, y\_0), (k\_1, y\_1), \dots, (k\_{m-1}, y\_{m-1})$ where each $k\_j$ has $\lceil \log\_2 n \rceil$ bits and each $y\_j$ has $\ell$ bits, check that $x\_{k\_j} = y\_j$ for all $j < m$. I claim that this can be done with $\tilde {O} ((n + m) \ell)$ additional variables and constraints.


First of all, we may append $(0, x\_0), (1, x\_1), \dots, (n-1, x\_{n-1})$ to the list $((k\_j, y\_j))$. Therefore we may assume without loss of generality that $m \geq n$ and $(k\_i, y\_i) = (i, x\_i)$ for $i < n$. Moreover, it is sufficient to check that $((k\_i, y\_i))$ is self-consistent: That if $k\_i = k\_j$ then $y\_i = y\_j$. This is checked by sorting $((k\_i, y\_i))$: Let $(\tilde {k}\_0, \tilde {y}\_0), \dots, (\tilde {k}\_{m-1}, \tilde {y}\_{m-1})$ be a permutation of $(k\_0, y\_0), \dots, (k\_{m-1}, y\_{m-1})$ with $\tilde {k}\_0 \leq \tilde {k}\_1 \leq \dots \leq \tilde {k}\_{m-1}$ (this is checkable in $\tilde {O} (m \ell)$ variables and constraints). Then it suffices to check the that if $\tilde {k}\_{i+1} = \tilde {k}\_i$ then $\tilde {y}\_{i+1} = \tilde {y}\_i$. This requires $O (m (\ell + \log n))$ bits and constraints.


