It is a spectrum.

Godel, Euler, Ramanujam, etc. didn't burn millions of dollars or drudged through search space like OpenAI's agent do to prove what they need.

Let's not forget using Lean as a crutch throughout the way rather than as a final tool for formalization and verification.