Formalization as suspension of intuition

Surprisingly, this echoes to me a recent thought: "frames blind us"; it comes to mind when I think of how traditional agent models (RL, game theory...) blinded us for years to their implicit assumption of no embeddedness [? · GW]. As with non-Euclidean shift, the change has come from relaxing the assumptions.
This post seems to complete your good old Traps of Formalization [AF · GW]. Maybe it's a hegelian dialectic: 
I) intuition domination (system 1)
II) formalization domination (system 2)
III) modulable formalization (improved system 1/cautious system 2)
Deconfusion is reached only when one is able to go from I to III.

I like this perspective! The idea of formalization as suspension of intuition reminds me of the story of the "Gruppenpest" in the development of quantum mechanics. The abstraction of groups (as well as representations and matrices) was seen by many as non-physical and unintuitive. But it turned out the resulting abstractions of gauge theories and symmetries were more fundamental objects than their predecessors.^[1][2][3][4]

It also reminds me of a view I've been told many times that mathematical formalization/modeling is the process of forgetting details about a problem until its essential character is laid bare. I think it's important to emphasize that formalization is only a partial suspension or redirection of intuition (which seems to be what Bachelard is actually implying), since the goal of formalization typically isn't to turn the process into something doable by a mechanical proof checker. Formalization removes all the "distractions" that block you from seeing underlying regularities, but you still need to leverage your intuition to get a grasp on those regularities. As you say in the post:

What this suspension gives us is a place to explore the underlying relationships and properties without the tyranny of immediate experience. Thus delivered from the “obvious”, we can unearth new patterns and structures that in turn alter our intuitions themselves!

1. ^{^}

   https://www.researchgate.net/publication/234207946_From_the_Rise_of_the_Group_Concept_to_the_Stormy_Onset_of_Group_Theory_in_the_New_Quantum_Mechanics_A_saga_of_the_invariant_characterization_of_physical_objects_events_and_theories

2. ^{^}

   https://ncatlab.org/nlab/show/Gruppenpest

3. ^{^}

   https://hsm.stackexchange.com/questions/170/how-did-group-theory-enter-quantum-mechanics

4. ^{^}

   https://www.math.columbia.edu/~woit/wordpress/?p=191

Upon reading the title I actually thought the article would argue the exact opposite, that formalization affects intuition in a negative way. I like non-eucledian geometry as a particular example where formalization actually helped discovery.

But this is definitely now always true. For instance if you wanted to intuitively understand why addition of naturals is commutative, maybe to build intuition for recognizing similar properties elsewhere, would this formal proof really help?

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_O m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n

This is as formal as it gets, a 100% machine checkable proof without room for human error.

I think formalization is just a tool that may or may not be helpful depending on your goal, and the real question is how you can tell ahead of time what level of formalization will be helpful?

I am not familiar with Bachelard, but I suspect that we understand how humans make progress in understanding the world rather better by now. 

But first, the very idea that formalization would have helped discover non-Euclidean geometries earlier seems counter to the empirical observation that Euclid himself formalized geometry with 5 postulates, how more formal can it get? Compared to the rest of the science of the time, it was a huge advance. He also saw that the 5th one did not fit neatly with the rest. Moreover, the non-Euclidean geometry was right there in front of him the whole time: spheres are all around. And yet the leap from a straight line to the great circle and realizing that his 4 postulates work just fine without the 5th had to wait some two millennia. 

In general, what you (he?) call "suspension of intuition", seems to me to be more like emergence of a different intuition after a lot of trying and failing. I think that the recently empirically discovered phenomenon of "grokking" in ML provides a better model of how breakthroughs in understanding happen. It is more of a Hegelian/Kuhnian model of phase transitions after a lot of data accumulation and processing. 

It is a fascinating topic, why in some cases these transitions happen quickly and in other cases take forever, and how they can be intentionally sped up. This is not necessarily grouped by field, either. Progress in fundamental physics was at breakneck speed in the first 30 years of the 20th century, then slowed down, and is at a crawl now, though glimpses of things to come are there again. Biology was stagnant since the times of Galen for a long time, then there was an age of breakthroughs. I suspect this applies to many other fields, as well. Psychology had a leap in Freud, and we are still not very far from his models. 

In retrospect, it does not feel like "formalization explicitly refuses to acknowledge our intuitions of things, the rich experience we always integrate into our concepts" is an essential step. It is more like "after a new concept emerges, it feels like it emerged after someone replaced intuition with formalization", but that was not the actual process that led to the emergence.

That's an interesting way of thinking about it. I'm reminded of how computers have revolutionized thought over the past century.

Most humans have tended to think primarily by intuition. Glorified pattern-matching, with all the cognitive biases that entails.

Computers, in contrast, have tended to be all formalization, no intuition. They directly manipulate abstract symbols at the lowest level, symbols that humans only deal with at the highest levels of conscious thought.

And now AI is bringining things back around to (surprisingly brittle) intuition. It will be interesting, at least, to see how newer AI systems will bring together formalized symbolic reasoning with pattern-matching intuition.