Re:New math book rescues landmark topology proof
by adgjlsfhk1 on Thursday September 09, 2021 @04:45PM
(#28474441)
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.
Re:New math book rescues landmark topology proof
by lostmsu on Thursday September 09, 2021 @05:47PM
(#28475054)
There 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.
I think you're mixing two different things here. Runtime is large for proof assistants, e.g. programs that can actually generate pieces of proof for you. Specifically the generation part. Verification of a complete proof were all the steps are provided like you would do in a paper should not, AFAIU, take a long time.