As always, this solution doesn't benefit from a blockchain structure. You could do the same thing with an immutable, publicly readable database.

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.

Where does that immutability come from? If you have a centralized service controlling the flow of knowledge, this could have its own consequences.

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)

> Where does that immutability come from? If you have a centralized service controlling the flow of knowledge, this could have its own consequences.

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.

Axioms can also be mutually contradictory and this may not be obvious initially. Then you can prove and disprove everything at the same time.

If axioms are mutually contradictory, that doesn't actually prevent the concept of computing them and attaching them to logical chains.

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.

Don't Gödel's incompleteness theorems show that this approach is impossible even for a domain as simple as arithmetic?

Science doesn’t need to be complete. It needs to be useful (that’s what I value in it).

Now you only need to convince the scientists to write proofs in their papers in Coq or Isabelle so that you can check them.

I basically work in mathematical physics and I'd like a system that allows me to write one thing, and output LaTeX code that can be put in a publication and also check the math.

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.

or Lean