ParentFull threadnicce·That is the point. Someone must verify that the Lean matches the actual theorem, precisely as it should be interpreted.View on HN