$ cd workspace/shared/lean_mathlib && lake env lean -E warning ../../../verified_math/F-192_erdos-267-faithful-theorem/Erdos267Standalone.lean
PASS (exit 0)
