Because Bitcoin and many other cryptocurrency mining certificates are "rare" in that their respective hash is less than a very small number, can we leverage their rarity in probabilistic proofs of other interesting problems?
In more detail, in Bitcoin mining miners compete to build a block by constructing a Merkle root of financial transactions, call it root $r$, and also finding a nonce, say nonce $c$, such that a cryptographic hash $H_S(r\Vert c)$, thought of as a number between $0$ and $1$, is less than a moving difficulty target $d$. (The hash is salted with other information $S$, such as the hash of the previous block; however, most of that extra information is constant for each block mined, hence I'm sweeping that under the rug for now.) Miners find such pairs $(r,c)$ about once every ten minutes. The adjustable difficulty $d$ is presently about $2^{-72}$. Thus, miners perform roughly $2^{71}$ hashes every ten minutes or so.
Furthermore, $r$ is $256$ bits while $c$ is $32$ bits. Accordingly, we can consider $r\Vert c$ as a $288$-bit number $q=2^{32}r+c$. A quick application of the prime number theorem suggests that this $288$-bit number is prime about once every $\log 2^{288}\approx 200$ blocks. This corresponds to a beacon of roughly one pair $(r,c)$ every 33 hours such that $q=2^{32}r+c$ is prime. (There may be other ways to increase the frequency of the beacon, e.g. by setting $q'=2^{33}r+2c+1$, etc., but for simplicity $q=2^{32}r+c$ suffices.)
For example, after a little bit of hunting on the main Bitcoin blockchain, at height 520605 Wolfram|Alpha confirms that the hexadecimal Merkle root and nonce
q:=c6b12a300769c930efd780c3c44f051099b1e447396d366426a04598819d467a||5838F735.
is prime.
We can say that not only is $q$ prime, but also $q$ is rare in that $H_S(q)$ is less than the small target $d$.
Furthermore, given a system $F=0$ of $k$ polynomial equations on $n$ variables, where the maximal degree over all monomials is $D$ and the bit-size of the largest coefficient is $h$, if the system is unsatisfiable in $\mathbb{C}^n$, unconditionally it will only be satisfiable modulo a finite number of prime $p$. Effective Nullstellensatz shows that for unsatisfiable systems without a solution in $\mathbb{C}^n$, there are at most
$$A_F=4n(n+1)D^n(h+\log k+(n+7)\log(n+1)D)$$
primes $p$ such that $F=0\mod p$.
However, if a system of polynomial equations in $\mathbb{C}$ is satisfiable then it will be satisfiable in $\mathbb{Z}/{p\mathbb{Z}}$ for a positive density of primes $p$. Assuming the Generalized Riemann Hypothesis, Koiran showed these primes $p$ will be distributed "evenly" across different equivalence classes, such that there is a "large" gap in good primes between satisfiable systems and unsatisfiable systems. This gap can be verified with only looking at the behavior of "small" primes.
Accordingly, Koiran proposes a protocol of certifying the satisfiability of the system over $\mathbb{C}$ by finding a rare prime $p$ such that both there is a solution to the given system in $\mathbb{Z}/{p\mathbb{Z}}$, and $H(p)=y$ for some randomly chosen hash $H$ and randomly chosen image $y$, where the size of the codomain of $H$ is chosen carefully such that there are enough candidate preimages $p$ to be able to invert the hash $H$ iff $F=0$ is satisfiable in $\mathbb{C}$.
Finally, as an example of using Bitcoin certificates in conjunction with Koiran's result, consider Chao and Gao's description of automated proofs of interesting geometric theorems. Given a problem in plane geometry, Chao and Gao construct systems of algebraic equations for the hypotheses and conclusion, and apply the Wu-Ritt method of characteristic sets to test whether the conclusion polynomial follows from the hypothesis polynomials.
For example, Chao and Gao prove Morley's theorem, which states that given any triangle $ABC$, trisectors of each angle $\angle ABC, \angle CAB, \angle BCA$ meet at an equilateral triangle $DEF$.
Chao and Gao provide a system of about $k=12$ equations in about $n=12$ variables, where the maximum degree $D=5$ and the maximal bit-complexity of the coefficients is $h=\log_2 6$. Thus, the Effective Nullstellensatz bound for Chao and Gao's description of Morley's Theorem is $A_F\le 2^{40}\ll 2^{72}$.
We can look for a solution in $\mathbb{F}_q^n$ to Chao and Gao's polynomials describing Morley's theorem, or, following Huang and Wong, we can decide that the system does have a solution in time $O(\log q)$ without necessarily finding the solution.
Hence, if one uses a SAT-solver to find a solution to Chao and Gao's system of equations for Morley's theorem in $\mathbb{F}_q^n$ for $q$ as the 288-bit prime root||nonce found above at the Bitcoin blockchain of height 520605, or if one uses Huang and Wong's approach, does one then have something close to a probabilistic proof of Morley's theorem, where the probability of being "wrong" is something like $d\times A_F\le 2^{-31}$ or so?
Comment: Even though I've rewritten this, I'm accepting DW's answer as helping to crystallize thinking.
