This proposal involves a possible path forward towards a decentralized system offering a degree-of-belief consensus on a non-trivial subset of all natural language statements, including those about reality.
Its possible uses include:
- Decentralized, formally verified scientific research aggregation.
- Automated literature review and meta-analysis.
- Proof- and incentive-assisted debate.
- Trustless fact-checking.
- Decentralized governance in arbitrary contexts.
The system would consist of three layers that would be designed and built sequentially, each extending the system’s capabilities upon implementation:
- Layer/phase 1: optimistic decentralized formal proof verification with reverse dependency tracking. Introduces all statements verifiable in the proof system.
- Layer/phase 2: formal definition and implementation of “extractors” and “injectors” mapping in and out of proofs via non-L1 “soft” axioms. Increases the scope to real-world statements not depending on real-world data.
- Layer/phase 3: incentive-based voting system for presumably non-provable statements, which would extract proofs about degree-of-belief statements and use them to update its state in a way that incentivizes informed belief.
This is a draft diagram of what the first layer could look like (each bubble represents a CIC expression, including proofs):
During initial testing, Coq could be used both for compilation of system components and verification (as part of the system itself). Afterwards, minimal ad hoc infrastructure could be set up and verified.
I began working on this about a month ago. I’ve already managed to extract formally verified contracts from Coq and tested a draft API for client code, so that’s a start.