@tomkalei You just have to hope that the machine doesn't find a proof of False and is using that as a lemma. @tao

https://mathstodon.xyz/@highergeometer/116196176162277025