Post #1258330

@tao On BlueSky, Kevin ( @xenaproject ) said you were collecting proofs of "650 implies 448" (or really, "650 implies xy=x"). I found a 27 step Prover9 proof and have just finished "humanizing" it. I did not look at the Vampire proof, but instead started from scratch, using methodology described in [1]. I'll just email you the LaTeX'ed PDF and the Prover9 proof itself. I don't speak Lean-ish so I can't do that conversion for you, but if someone wants to take it on, it's fine with me. [1] M. Kinyon, Proof simplification and automated theorem proving, Philos. Trans. Roy. Soc. A, 377 (2019), no. 2140, 20180034, 9 pp. arXiv version: https://arxiv.org/abs/1808.04251