Are there any AI generated proofs that are simple enough to be verified quickly by a human, that have not been lean verified? Or are they all basically incomprehensible?
[1] https://github.com/openai/math/blob/main/preprints/An-Almost... [2] https://github.com/openai/math/blob/main/lean/ComparatorChal...