I think this could be a great application for a DAG blockchain, with the axioms of a given scientific field as initial seed blocks.
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”
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.
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.
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.
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”