> John Baez's This Week's Finds posts

As an aspiring amateur of recreational mathematics, it gives me joy to find this recommendation and start reading the series. It reminds me of Martin Gardner's "Mathematical Games" column, and its successor, Douglas Hofstadter's "Metamagical Themas".

For a while now I've been chewing on Baez's paper, "Physics, Topology, Logic and Computation: A Rosetta Stone". I'm intrigued by it. At first baffled, then continued studying related topics, coming back to re-read and appreciate what it's saying. I'm exploring what it means from the computation angle, in the context of Haskell Curry, combinators, lambda calculus, cellular automata, rewriting systems. And more far-fetched thoughts, like Stephen Wolfram, Max Tegmark, or how it may relate to biology such as Michael Levin's research.

On the role of AI in mathematics, it brings up more questions about the use of computers in experimental/exploratory mathematics. Part of the concensus emerging, it seems, is the formalization of programs as proofs, in particular the Lean language ecosystem. It's like the field of software engineering is rediscovering its roots.

The deeper I go the more I want to participate, write and talk about the fun things I'm discovering. Maybe one day write a paper of my own, if I can manage to do it in a respectable rigorous manner. For that I know I still have a lot of basics to learn, cultural etiquette too, and probably lean on something like Lean to be able to demonstrate that the ideas are sound.