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?
Completely agree! The point is not that formalization or axiomatization is always good, but rather to elucidate one counterintuitive way in which it can be productive, so that we can figure out when to use it.
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?
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?
Completely agree! The point is not that formalization or axiomatization is always good, but rather to elucidate one counterintuitive way in which it can be productive, so that we can figure out when to use it.
Also I just found that you already argued this in an earlier post, so I guess my point is a bit redundant.
Anyway, I like that this article comes with an actual example, we could probably use more examples/case studies for both sides of the argument.