This is exactly why I submitted [1] to HN, coincidentally a few hours ago. IMO, assertions should be computable (if possible) and backed by data.
Then any proofs can be derived using the previous blocks, and, should any proof be disproved the whole sub chain depending on it would collapse and need to be rewritten “remined”
The currently unsolvable problem is that there is often disagreement about axioms and proofs bring disproved. Even mathematical proofs can be very controversial.
This is one of many problems that humans can't solve yet, which means it's hard/impossible to teach computers to do it.
The core problem with computing them is that no machine can decide whether the axioms are contradictory in the first place. In most cases, even humans won't 100% agree.
Maybe some sort of CRDT + gossip network? But at that point you are quite close to a blockchain.
(Not that I'm confident such a thing is a good idea, but I do think that a decent portion of the blockchain stack makes sense given the idea)
Data can be:
- decentralized
- public
- immutable
- redundant
- verifiable with asymmetric cryptography
..without being part of a blockchain. The technology to do this has existed much longer than blockchain has as a concept. Torrents are a good example.
Coq and the like seem way too "low-level". I'm sure it's possible in principle to handle proofs involving partial differential equations in Coq but it surely is not easy.