If you’re interested in applications of AI to mathematics, you’re faced with the problem of what to do when the ratio of plausible proofs to humans that can check them radically changes. There are definitely some in the AI world who feel that the existing highly social construct of informal mathematical proof will remain intact, just with humans replaced by agents, but amongst mathematicians there is a growing realization that formalization is the best way to deal with this epistemological crisis.

It helps that work done in Lean (on Mathlib and other developments) is reaching an inflection point just as these questions become practically relevant from AI.

It's not AI in itself, but it's one of the best possibilities for enabling AI systems to generate mathematical proofs that can be automatically verified to be correct, which is needed at the scale they can potentially operate.

Of course it has many non-AI uses too.

Proof automation definitely counts as AI. Not all AI is based on machine learning or statistical methods, GOFAI is a thing too.

If you want to have superhuman performance like AlphaZero series you need a verifier (valuation network) to tell you if you are on the right track. Lean (proof checker) in general can act as a trusted critic.

They do have AI on their roadmap, though: https://lean-fro.org/about/roadmap-y2/

Seems more like applying LEAN to AI development, no?

Partially, I guess, but also: "We will seek to provide tooling, data, and other support that enables AI organizations and researchers to advance Lean’s contribution at the intersection of AI, math, and science."

It's not ML, but it is AI