@tao@mathstodon.xyz Your recent blog post on the Jacobian Conjecture + these slides + your answers in this AI "interview" have done a fantastic job of painting a more hopeful picture of the future of AI use in mathematics (at least for me). I think this hope is especially kindled by finally seeing this topic of "foundations of practice" being taken up in earnest. You have talked about this in the past, but this is the first time I have seen it taken up with some eye towards being partially tractable with the tools of logic/math (instead of relying solely on empiricism). I personally think this will increasingly become more precise and more than a heuristic analogy. Explicitly stating the "Working Hypothesis" in a precise way is a great thing to do. This sort of clarity is extremely important and I think will help guide the discussion in more helpful directions. Like you mentioned, this shouldnt take away from your overall points, (which I think are absolutely fantastic), but I have one comment about this hypothesis. The analogy I might give is with the previous crisis in foundations. Classical geometry was "solved" by the notion of computability, but new problems arose that made the equivalent of the "working hypothesis" false anyways. Similarly, what is meant by "Research level mathematics" now could change and render the "working hypothesis" false in the future, even if it is true right now. This has been my primary issue with this hypothesis and I haven't had the chance to state this objection clearly since it is rarely explicitly stated. I.e. if even a small subset of problems are not AI tractable but are tractable by humans, then the "reasonably strong" form is likely to collapse to the "weak" form.