[rmrfstar]

I see what you're saying.

I think the author meant the same thing as Feynman when he described the "Greek" and "Babylonian" approaches to mathematics.

For all but a select few (pure mathematicians), the "Babylonian" approach is a lot more fun. Both approaches are clearly necessary and useful in different settings.

With the advent of systems like the Lean theorem prover, the two approaches may start to see a lot more overlap.