Huh, I hadn't heard of that. The controversy around it is... interesting.
The controversy around AM is the same as around Eurisko, right? that it's not clear how much was the AI and how much was Lenat. I believe that Lenat says the Traveller fleet design was 60% Lenat and 40% Eurisko. It's not clear what it means to quantify that, so it's not clear that he disagrees with the skeptics. In fact, his abandonment of Eurisko suggests that he agrees. Here's the OB discussion of Lenat.
Suppose we made an algorithm capable of forming empirical conjectures for mathematics. How might such an algorithm discover the principle of mathematical proof?
I would like to see an article on the relevant philosophy and mathematical logic background for this problem. Since I currently lack the inclination to research and write up such an article, I instead made this post.