3 ms·
The problem is that the way people write proofs, you don't go axiom by axiom. You might evaluate an integral in one step, or make an argument that some sequence
by adgjlsfhk1 5y ago
The problem is that the way people write proofs, you don't go axiom by axiom. You might evaluate an integral in one step, or make an argument that some sequence is obviously asymptotically less than a function. Pretty much every step in a human proof requires a computer proof generation step to verify.
- lostmsu 5y agoThere might be a chicken and an egg problem. If knowledge of theoretical mathematics would be designed like a framework with good documentation what you mention would be solved by simply referring to the corresponding part of the framework. But to get that more people would need to be involved into transcribing proofs into formal language. Ideally, everyone. This is a higher standard, and somebody needs to ask for it.