Comment by opan

I'm relieved that Lean4 doesn't seem to be some AI thing.