The file SSOT.lean is completely trivial, I think: Unfolding the definitions in the theorems, they say nothing but "x=1 => x=1", "x=1 => x≤1", and "x≠1 => x=0 ∨ x>1" (where x is a natural number). Basically, there's no actual proof here, at least not in that file....
This is indeed the danger of letting LLMs manage a "proof" end-to-end—they can just pick the wrong definitions and theorems to prove, and even though the proofs they then give will be formally sound, they won't prove anything useful.
This is indeed the danger of letting LLMs manage a "proof" end-to-end—they can just pick the wrong definitions and theorems to prove, and even though the proofs they then give will be formally sound, they won't prove anything useful.