Putting Metamath on Ethereum

[void4]

It would be interesting to put a Metamath proof verifier on the Ethereum chain. This would allow anyone to set ETH/ERC20/ERC721/arbitrary other rewards on the solution of open problems.

For more, see: Proofcoin: A reward system for proof solving #65

Is Solidity the right language for this?

Maybe. The Metamath stack machine is quite simple

However, waiting for eWasm (Webassembly) support could make the implementation easier and allow for reuse of, say, the existing Rust Metamath verifier.

What if no one finds a proof or the contract remains unused

Make reward deposits time limited (but with long-term minimums, like 1 year, so people can plan research long term).

Gas costs: Instruction steps

Verifying the existing metamath set.mm database from scratch requires several million substitutions -> millions of EVM instructions.

Gas costs: Memory - The main ZFC database, set.mm, requires 30MB of storage

This would incur storage costs in the tens of thousands of dollars. Possible approaches include:

• prepopulating the contract with preaccepted proofs (but only their inputs and outputs, not their proofs, this may be a few hundred Kilobytes)
• store the merkle hash of set.mm in the contract, let user supply path with associated proofs in transaction
• instead of string labels, use integers
• only store a subset, the most commonly referenced proofs
• (future) use zksnarks

Variant	Compression	Size (KB)
set.mm (with comments and compressed proofs)	-	32900
	.zip	11400
proof statements only (without hypotheses)	-	2200
	.zip	317
	Huffman coding (words)	614
	Huffman coding (characters)	1140

Frontrunning

"Ethereum is a Dark Forest" highlights the adverse environment of the public tx mempool. Frontrunning can be avoided by

• cooperating directly with a miner (tradeoffs: trust, speed)

• splitting/obfuscating the transaction in some way

It may be possible for the submitter to send a hash of the solution plus a random nonce to the chain first, when that tx is confirmed to be the first with that hash on the contract (to avoid direct frontrunning, and fork-frontrunning, with multi-block confirmation times to prevent block reorgs by potentially adversarial miners) submit the solution and nonce in a second tx.

Edit: JT proposed just hashing the solution with the sender address, which avoids the frontrunning problem altogether, one just has to check if the transaction was successfully executed on the chain!

Problem: that's a lot of hashing!

Conclusion

Right now doesn't seem to be quite the right time to do this, mm0 is still in development and not fully formalized, programming (any) verifier in Solidity is hard, and putting and running anything like it on the Ethereum chain is too expensive as of now. Alternatives should be considered (different/new blockchain, or (partially) centralized systems).