A Neuro-Symbolic engine that autonomously verified the GCT barrier in Lean 4 | Heykuki News