Comment by practal

This interplay between intuition and logic is exactly what makes the magic happen. You need intuition to feel your way forward, and then logic to solidify your progress so far, and also for ideas maybe not directly accessible via intuition only. I've experienced that myself, and it is even well-documented, because I wrote technical reports and such at each stage. My discovery of Abstraction Logic went through various stages:

1) First, I had a vague vision of how I want to do mathematics on a computer, based on my experience in interactive theorem proving, and what I didn't like about the current state of affairs: https://doi.org/10.47757/practal.1

2) Then, I had a big breakthrough. It was still quite confused, but what I called back then "first-order abstract syntax" already contained the basic idea: https://obua.com/publications/practical-types/1/

3) I tried to make sense of this then by developing abstraction logic: https://doi.org/10.47757/abstraction.logic.1 . After a while I realized that this version only allowed universes consisting of two elements, because I didn't distinguish between equality and logical equality, which then led to a revised version: https://doi.org/10.47757/abstraction.logic.2

4) My work so far was dominated by intuition based on syntax, and I slowly understood the semantic structures behind this: the mathematical universe consisting of values, and operations and operators on top of that: https://obua.com/publications/philosophy-of-abstraction-logi...

5) I started to play around with this version of abstraction logic by experimenting with automating it, giving a talk about it at a conference, (unsuccessfully) trying to publish a paper about it, and implementing a VSCode plugin for it. As a result of using that plugin I realized that my understanding until now of what axioms are was too narrow: https://practal.com/press/aair/1/

6) As a consequence of my new understanding, I realized that besides terms, templates are also essential: https://arxiv.org/abs/2304.00358

7) I decided to consolidate my understanding through a book. By taking templates seriously from the start when writing, I realized their true importance, which led to a better syntax for terms as well, and to a clearer presentation of Abstraction Algebra. It also opened up my thinking of how Abstraction Algebra is turned into Abstraction Logic: https://practal.com/abstractionlogic/

8) Still lots of stuff to do ...

I would not be surprised if that is exactly the way forward for AIs as well. They clearly have cracked (some sort of) intuition now, and we now need to add that interplay between logic and intuition to the mix.