* Pure mathematics: Consider e.g. the difficulty in verifying the recent proofs of Fermat's Last Theorem (Wiles-Taylor-Frey theorem?), the Poincaré conjecture (Perelman-Hamilton-Thurston theorem?), and now the ABC conjecture (Mochizuki-Szpiro theorem?): there is essentially no indication of the correctness of a mathematical proof besides simply having a whole lot of smart people look at it and think very hard. This may be of particular interest because pure math has lately experienced a turn towards the use of proof-verifying systems, and so it may be of some interest if one of these can be designed for cryptography.
In particular, consider the following method of verification: a cryptographically secure function h(M, k), known or at least believed to be hard, a message M, a secret key k, and a channel C(h) over which data is transmitted. We wish to prove the following combination of statements: a: given C and h, a method to obtain the message M also obtains the key k, and b: given M, C, and h, it is "impossible" to obtain the key k -- i.e. it would require breaking the hash function; this means that if the cryptography is broken, so must be the hash function. The latter portion of the proof is necessary because we must always consider the possibility of a rubber hose or a stupid user.
EDIT: I should add here that side channel attacks depend on an incorrect understanding of the content of C. So perhaps we should include c: we send only what we wish to in C.
In the interest of pedantry, I dreamed up an example "cryptosystem" which may fit the bill, though I have no honest idea of the difficulty of the h function [and I know almost nothing about cryptography!]: consider a large prime number p, the finite field F_p, and its algebraic closure Fbar_p. A message M is a [presumaly long] polynomial M(x) over Fbar_p, and a key consists of the pair k = [p, z], where z is some arbitrary element of Fbar_p. h(M, k) is obtained by expanding (x - z) * M(x) in Fbar_p, and we send over C the coefficients of the resulting polynomial. Verification is obtained by computing C(z) in Fbar_p and the message is extracted by polynomial division. Then (a) rests on the difficulty of factoring a polynomial and (b) rests on the secrecy of p: so we cannot, for example, simply compute C/M.
Note that Fbar_p is countable, so the whole procedure uses only integer math.
If I understood your proposed system correctly, the following seems to be a deal-breaking weakness: Given a number of polynomials representing encrypted messages, (x-z) is a common factor of all of them. The GCD of a set of polynomials can very efficiently be computed. Thus, an attacker observing different messages encrypted with the same key over time gets a better and better idea of what the key is (how quickly depends on the messages: two plaintext messages that happen to give coprime polynomials M_1(x) and M_2(x) would be enough to get the key).
In this case, simply computing the GCD may require "non-obvious" intuition, since the polynomials do not act over the real numbers, but the algebraic closure of an unknown finite field. But I wouldn't bet my data on it, at least, not until I am a lot more confident in my understanding of abstract algebra.
Two notes: factoring polynomials over finite fields isn't hard (look up the Berlekamp algorithm or Cantor-Zassenhaus for starters). Second, I believe the system you've described doesn't satisfy your property (b). Quantities such as M[1]C[0] - C[1]M[0] + M[0]^2 and C[1]M[2] - C[2]M[1] + M[1]^2 - M[0]M[2] are congruent to 0 mod p; compute them over the integers and then take the gcd. By computing enough of these you should recover the prime p. Once you have p, recovering z is very easy (e.g., take the gcd of C and C'-M, where C' is the derivative of C).
I feel a major problem with mathematical proofs is that the language of these proofs is so complex that in order to understand what it even says you have to be extremely smart, and willing to put in a huge amount of time in the first place.
A proof is in effect a "program" that describes the logical conditions of whatever it is trying to show. Invalid proofs are those with "bugs". Perhaps if the language of math was a bit clearer, it would not be such a difficult to understand field.
* Pure mathematics: Consider e.g. the difficulty in verifying the recent proofs of Fermat's Last Theorem (Wiles-Taylor-Frey theorem?), the Poincaré conjecture (Perelman-Hamilton-Thurston theorem?), and now the ABC conjecture (Mochizuki-Szpiro theorem?): there is essentially no indication of the correctness of a mathematical proof besides simply having a whole lot of smart people look at it and think very hard. This may be of particular interest because pure math has lately experienced a turn towards the use of proof-verifying systems, and so it may be of some interest if one of these can be designed for cryptography.
In particular, consider the following method of verification: a cryptographically secure function h(M, k), known or at least believed to be hard, a message M, a secret key k, and a channel C(h) over which data is transmitted. We wish to prove the following combination of statements: a: given C and h, a method to obtain the message M also obtains the key k, and b: given M, C, and h, it is "impossible" to obtain the key k -- i.e. it would require breaking the hash function; this means that if the cryptography is broken, so must be the hash function. The latter portion of the proof is necessary because we must always consider the possibility of a rubber hose or a stupid user.
EDIT: I should add here that side channel attacks depend on an incorrect understanding of the content of C. So perhaps we should include c: we send only what we wish to in C.
In the interest of pedantry, I dreamed up an example "cryptosystem" which may fit the bill, though I have no honest idea of the difficulty of the h function [and I know almost nothing about cryptography!]: consider a large prime number p, the finite field F_p, and its algebraic closure Fbar_p. A message M is a [presumaly long] polynomial M(x) over Fbar_p, and a key consists of the pair k = [p, z], where z is some arbitrary element of Fbar_p. h(M, k) is obtained by expanding (x - z) * M(x) in Fbar_p, and we send over C the coefficients of the resulting polynomial. Verification is obtained by computing C(z) in Fbar_p and the message is extracted by polynomial division. Then (a) rests on the difficulty of factoring a polynomial and (b) rests on the secrecy of p: so we cannot, for example, simply compute C/M.
Note that Fbar_p is countable, so the whole procedure uses only integer math.