> people believe is true, but cannot build upon because they don't fully understand it. OK, maybe it doesn't help people build on the proof, but does it help c

> people believe is true, but cannot build upon because they don't fully understand it. OK, maybe it doesn't help people build on the proof, but does it help computers build on the proof? Why does it have to come back to human understanding? Maybe it's not possible right now for computers to generalize proof strategies, but I wouldn't bet against it becoming possible down the road.